src/HOL/Library/Quotient_Syntax.thy
changeset 37951 4e2aaf080572
parent 35787 afdf1c4958b2
child 40602 91e583511113