[isabelle] Duplicate algebra tactic



Currently, both HOL.Groebner_Basis and HOL-Algebra.Ring provide an
`algebra' tactic. This means that importing Ring (or any theory that
depends on it) breaks proofs that use the algebra tactic, which is
highly non-intuitive.

(Thanks to Bertram for helping me diagnose this.)

Perhaps Ring.algebra should be renamed? I think "ringsimp" would work
well as an alternative name.

Kind regards,
Jakub Kądziołka




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