src/Pure/Syntax/syn_trans.ML
changeset 14024 213dcc39358f
parent 13762 9dd78dab72bc
child 14647 3f9d3d5cd0cd