src/HOL/ex/IntRing.ML
changeset 9436 62bb04ab4b01
parent 5227 e5a6ace920a0