src/Pure/Syntax/syntax.ML
changeset 25111 d52a58b51f1f
parent 25060 17c313217998
child 25122 f37d7dd25c88