src/HOL/Algebra/QuotRing.thy
changeset 20848 27a09c3eca1f
parent 20318 0e0ea63fe768
child 21502 7f3ea2b3bab6