src/HOL/Library/Quotient_Syntax.thy
changeset 38187 fd28328daf73
parent 35787 afdf1c4958b2
child 40602 91e583511113