src/HOL/Algebra/QuotRing.thy
changeset 77901 5728d5ebce34
parent 77138 c8597292cd41
child 80914 d97fdabd9e2b