src/HOL/mono.ML
changeset 4208 b67223fddc11
parent 4159 4aff9b7e5597
child 5100 68775c0e40e7
equal deleted inserted replaced
4207:061919f8da9c 4208:b67223fddc11