src/Pure/Syntax/syntax.ML
changeset 25261 3dc292be0b54
parent 25122 f37d7dd25c88
child 25387 d9ab1e3a8acb