src/HOL/Algebra/ringsimp.ML
changeset 30056 0a35bee25c20
parent 29269 5c25a2012975
child 30510 4120fc59dd85