Re: [isabelle] HOL-Algebra breaks "algebra" method

I decided to look into the matter myself after all and found the
problem: the "normal" algebra method we all know and love is declared in
"Groebner_Basis", but HOL-Algebra also declares an "algebra" method that
shadows the other one.

Of course, one can still access both of them using the fully-qualified
names Ring.algebra and Groebner_Basis.algebra. Still, in my opinion, it
may a good idea to resolve this naming conflict.

For instance, the situation is that currently, proofs using the
"algebra" method break once HOL-Number_Theory is imported (since it
depends on some theories from HOL-Algebra)



On 20/10/16 15:50, Manuel Eberl wrote:
> 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

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.