src/Pure/Syntax/syn_trans.ML
changeset 41111 b497cc48e563
parent 40235 87998864284e
child 42043 2055515c9d3f
equal deleted inserted replaced
41110:32099ee71a2f 41111:b497cc48e563