src/HOL/Algebra/ringsimp.ML
changeset 30562 7b0017587e7d
parent 30528 7173bf123335
child 30722 623d4831c8cf