*To*: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*Subject*: [isabelle] HOL-Algebra breaks "algebra" method*From*: Manuel Eberl <eberlm at in.tum.de>*Date*: Thu, 20 Oct 2016 15:50:57 +0200*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.4.0

Hallo, I just noticed the following odd behavior: the "algebra" proof method seems to stop working whe ~/src/HOL/Algebra/Ring is imported. This does not seem to be a regression either; the same problem occurred in Isabelle2016. Example: theory Test imports Main "~~/src/HOL/Algebra/Ring" begin lemma fixes a b :: nat shows "a * b = b * a" by algebra end (when the ~~/src/HOL/Algebra/Ring import is removed, everything works) Any ideas, anyone? Manuel

**Follow-Ups**:**Re: [isabelle] HOL-Algebra breaks "algebra" method***From:*Manuel Eberl

- Previous by Date: [isabelle] Isabelle document prep and ACM journals document class
- Next by Date: [isabelle] Haskell code generation for Imperative/HOL
- Previous by Thread: Re: [isabelle] [ExternalEmail] Isabelle document prep and ACM journals document class
- Next by Thread: Re: [isabelle] HOL-Algebra breaks "algebra" method
- Cl-isabelle-users October 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list