src/HOL/Quotient.thy
changeset 51518 6a56b7088a6a
parent 51112 da97167e03f7
child 53011 aeee0a4be6cf