src/Pure/Syntax/syn_trans.ML
changeset 28962 f603183f7a5c
parent 28856 5e009a80fe6d
child 29276 94b1ffec9201
equal deleted inserted replaced
28961:9f33ab8e15db 28962:f603183f7a5c