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.