src/HOL/Algebra/ringsimp.ML
changeset 35721 f7bbee848403
parent 35408 b48ab741683b
child 35849 b5522b51cb1e