src/HOL/Library/Quotient_Syntax.thy
changeset 39214 49fc6c842d6c
parent 35787 afdf1c4958b2
child 40602 91e583511113