src/HOL/Algebra/QuotRing.thy
changeset 21404 eb85850d3eb7
parent 20318 0e0ea63fe768
child 21502 7f3ea2b3bab6