src/Pure/Syntax/syn_trans.ML
changeset 1228 7d6b0241afab
parent 1178 b28c6ecc3e6d
child 1326 1fbf9407757c
equal deleted inserted replaced
1227:c9f7848bc5ee 1228:7d6b0241afab