src/HOL/Algebra/QuotRing.thy
changeset 22277 b89dc456dbc6
parent 21502 7f3ea2b3bab6
child 23350 50c5b0912a0c