src/Pure/Syntax/syn_trans.ML
changeset 41070 36cec0e3491f
parent 40235 87998864284e
child 42043 2055515c9d3f
equal deleted inserted replaced
41069:6fabc0414055 41070:36cec0e3491f