src/HOL/Algebra/QuotRing.thy
changeset 21461 51239d45247b
parent 20318 0e0ea63fe768
child 21502 7f3ea2b3bab6