src/HOL/Quotient.thy
changeset 40476 515eab39b6c2
parent 40466 c6587375088e
child 40602 91e583511113