src/HOL/Algebra/QuotRing.thy
changeset 58656 7f14d5d9b933
parent 45005 0d2d59525912
child 61382 efac889fccbc