src/HOL/Algebra/ringsimp.ML
changeset 47647 ec29cc09599d
parent 45625 750c5a47400b
child 47701 157e6108a342