src/Pure/Syntax/syn_trans.ML
changeset 1868 836950047d85
parent 1511 09354d37a5ab
child 2698 8bccb3ab4ca4