src/HOL/Tools/Quotient/quotient_typ.ML
changeset 39812 cdee5ca9ba9e
parent 39288 f1ae2493d93f
child 41444 7f40120cd814
equal deleted inserted replaced
39811:0659e84bdc5f 39812:cdee5ca9ba9e