src/Pure/Thy/thy_syntax.ML
changeset 33092 c859019d3ac5
parent 30573 49899f26fbd1
child 36950 75b8f26f2f07