[isabelle] HOL-Algebra breaks "algebra" method
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
imports Main "~~/src/HOL/Algebra/Ring"
fixes a b :: nat
shows "a * b = b * a" by algebra
(when the ~~/src/HOL/Algebra/Ring import is removed, everything works)
Any ideas, anyone?
This archive was generated by a fusion of
Pipermail (Mailman edition) and