src/Pure/Thy/thy_syntax.ML
changeset 52516 b5b3c888df9f
parent 51423 e5f9a6d9ca82
child 53843 88c6e630c15f