src/HOL/Algebra/QuotRing.thy
changeset 22744 5cbe966d67a2
parent 21502 7f3ea2b3bab6
child 23350 50c5b0912a0c