src/HOL/Algebra/ringsimp.ML
changeset 46099 40ac5ae6d16f
parent 45625 750c5a47400b
child 47701 157e6108a342