src/HOL/ex/IntRingDefs.thy
changeset 8702 78b7010db847
parent 5601 b6456ccd9e3e