src/HOL/Algebra/IntRing.thy
changeset 24077 e7ba448bc571
parent 23957 54fab60ddc97
child 24131 1099f6c73649