src/HOL/Algebra/ringsimp.ML
changeset 35043 07dbdf60d5ad
parent 33520 b2cb4da715f7
child 35408 b48ab741683b