src/Pure/type_infer.ML
changeset 80264 71c1cf9e7413
parent 79433 88341f610b33
child 81259 1c2be1fca2bd
equal deleted inserted replaced
80263:8a0ccdcae2d1 80264:71c1cf9e7413