src/HOL/ex/IntRingDefs.ML
changeset 5228 66925577cefe
parent 5227 e5a6ace920a0
child 5601 b6456ccd9e3e