src/Pure/type_infer.ML
changeset 15134 d3fa5e1d6e4d
parent 14993 802f3732a54e
child 15531 08c8dad8e399
equal deleted inserted replaced
15133:87c074aad007 15134:d3fa5e1d6e4d