src/Pure/type_infer.ML
changeset 4273 c9b577c8f7a1
parent 3784 3b15cda31c97
child 4957 30c49821e61f
equal deleted inserted replaced
4272:61c6ae12ca14 4273:c9b577c8f7a1