src/HOL/Quotient.thy
changeset 78851 db37cae970a6
parent 76923 8a66a88cd5dc
child 80676 32073335a8e9
equal deleted inserted replaced
78850:3069da1743bc 78851:db37cae970a6