src/HOL/Library/Quotient_Syntax.thy
changeset 38244 59484a20c48f
parent 35787 afdf1c4958b2
child 40602 91e583511113