src/Pure/Thy/thy_syntax.ML
changeset 29360 a5be60c3674e
parent 29319 592503fd6dad
child 30573 49899f26fbd1