src/HOL/ex/IntRingDefs.thy
changeset 5526 e7617b57a3e6
parent 5491 22f8331cdf47
child 5601 b6456ccd9e3e