src/Pure/Thy/thy_syntax.ML
changeset 40419 718b44dbd74d
parent 40290 47f572aff50a
child 40523 1050315f6ee2