src/Pure/Thy/thy_syntax.ML
changeset 41058 42e0a0bfef73
parent 40958 755f8fe7ced9
child 41484 51310e1ccd6f