src/HOL/Algebra/ringsimp.ML
changeset 67519 6905b156a030
parent 58811 19382bbfa93a
child 67560 0fa87bd86566