src/HOL/Library/Quotient_Syntax.thy
changeset 39109 ceee95f41823
parent 35787 afdf1c4958b2
child 40602 91e583511113