src/Pure/Syntax/syn_trans.ML
changeset 1626 12560b3ebf2c
parent 1511 09354d37a5ab
child 2698 8bccb3ab4ca4