src/HOL/Algebra/ringsimp.ML
changeset 21526 1e6bd5ed7abc
parent 21505 13d4dba99337
child 21588 cd0dc678a205