src/Pure/type_infer.ML
changeset 58821 11e226e8a095
parent 53672 df8068269e90
child 62958 b41c1cb5e251
equal deleted inserted replaced
58820:3ad2759acc52 58821:11e226e8a095