src/Pure/Syntax/syn_trans.ML
changeset 14838 b12855d44c97
parent 14798 702cb4859cab
child 14868 617e4b19a2e5
equal deleted inserted replaced
14837:827c68f8267c 14838:b12855d44c97