src/Pure/type_infer.ML
changeset 70823 c6f2a73987cd
parent 69575 f77cc54f6d47
child 74220 c49134ee16c1
equal deleted inserted replaced
70822:22e2f5acc0b4 70823:c6f2a73987cd