src/Pure/Syntax/syn_trans.ML
changeset 2348 b51e104ecf40
parent 1511 09354d37a5ab
child 2698 8bccb3ab4ca4