src/HOL/Algebra/QuotRing.thy
changeset 27094 2cf13a72e170
parent 23463 9953ff53cc64
child 27611 2c01c0bdb385