src/HOL/ex/IntRingDefs.thy
changeset 7333 6cb15c6f1d9f
parent 5601 b6456ccd9e3e