src/HOL/Algebra/QuotRing.thy
changeset 62611 dc7cc407c911
parent 61382 efac889fccbc
child 63040 eb4ddd18d635