src/Pure/Thy/thy_syntax.ML
changeset 61127 76cd7f1ec257
parent 59809 87641097d0f3
child 61379 c57820ceead3