src/Pure/Thy/thy_syntax.ML
changeset 57907 7fc36b4c7cce
parent 57905 c0c5652e796e
child 58864 505a8150368a