src/HOL/ex/IntRingDefs.ML
changeset 5253 82a5ca6290aa
parent 5227 e5a6ace920a0
child 5601 b6456ccd9e3e