src/Pure/Syntax/syn_trans.ML
changeset 14838 b12855d44c97
parent 14798 702cb4859cab
child 14868 617e4b19a2e5