src/Pure/Syntax/syn_trans.ML
changeset 19960 a0e3f2df9b0e
parent 19848 a525275d36df
child 20076 def4ad161528
equal deleted inserted replaced
19959:dc3e007aeaf1 19960:a0e3f2df9b0e