src/HOL/mono.ML
changeset 2404 edcc26b1461d
parent 1849 bec272e3e888
child 2922 580647a879cf
equal deleted inserted replaced
2403:8115988ccc22 2404:edcc26b1461d