[isabelle] HOL-Algebra breaks "algebra" method



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.