src/Pure/Syntax/syn_trans.ML
changeset 15969 201f6738480f
parent 15570 8d8c70b41bab
child 16612 48be8ef738df
equal deleted inserted replaced
15968:c4e8a6af2235 15969:201f6738480f