src/Pure/Thy/thy_syntax.ML
changeset 68482 cb84beb84ca9
parent 61379 c57820ceead3