src/Pure/Thy/thy_syntax.ML
changeset 33930 6a973bd43949
parent 30573 49899f26fbd1
child 36950 75b8f26f2f07