src/Pure/type_infer.ML
changeset 80224 db92e0b6a11a
parent 79433 88341f610b33
child 81259 1c2be1fca2bd
equal deleted inserted replaced
80223:d389577a6fba 80224:db92e0b6a11a