Email Gateway (Oct 07 2020 at 14:13): Email Gateway (Oct 07 2020 at 14:13):From: Jakub Kądziołka <kuba@kadziolka.net>
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
Last updated: Jan 04 2025 at 20:18 UTC