src/HOL/Quotient.thy
changeset 44345 881c324470a2
parent 44242 a5cb6aa77ffc
child 44413 80d460bc6fa8