src/HOL/ex/IntRingDefs.thy
changeset 8039 a901bafe4578
parent 5601 b6456ccd9e3e