src/HOL/mono.ML
changeset 5148 74919e8f221c
parent 5100 68775c0e40e7
child 5316 7a8975451a89
equal deleted inserted replaced
5147:825877190618 5148:74919e8f221c