src/Pure/Thy/thy_parse.ML
changeset 1868 836950047d85
parent 1850 c6b6ccfd390c
child 2203 c2dbdc2ef781