src/Pure/Syntax/syntax.ML
changeset 1559 9ba0906aa60d
parent 1511 09354d37a5ab
child 1580 e3fd931e6095