src/Pure/Thy/thy_parse.ML
changeset 1597 54ece585bf62
parent 1555 a5f48457dfd5
child 1705 19fe0ab646b4