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