src/HOL/Algebra/ringsimp.ML
changeset 48391 480746f1012c
parent 47701 157e6108a342
child 51717 9e7d1c139569