src/HOL/Library/Quotient.thy
changeset 27885 76b51cd0a37c
parent 27487 c8a6ce181805
child 29608 564ea783ace8