src/HOL/Algebra/ringsimp.ML
changeset 59842 9fda99b3d5ee
parent 58811 19382bbfa93a
child 67560 0fa87bd86566