src/HOL/Algebra/ringsimp.ML
changeset 50805 69439c9defec
parent 47701 157e6108a342
child 51717 9e7d1c139569