# 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)
Cheers,
Manuel
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.*