src/HOL/Library/Quotient_Syntax.thy
changeset 35567 309e75c58af2
parent 35222 4f1fba00f66d
child 35787 afdf1c4958b2