src/Pure/Thy/thy_parse.ML
changeset 3895 b2463861c86a
parent 3875 f62a4edb1888
child 3900 e30bd27a4910