src/Pure/Thy/thy_syntax.ML
changeset 52344 ff05e50efa0d
parent 51423 e5f9a6d9ca82
child 53843 88c6e630c15f