src/HOL/ex/IntRingDefs.thy
changeset 7567 62384a807775
parent 5601 b6456ccd9e3e