src/Pure/Thy/thy_syntax.ML
changeset 32261 05e687ddbcee
parent 30573 49899f26fbd1
child 36950 75b8f26f2f07