src/Pure/Isar/outer_syntax.ML
changeset 7632 25a0d2ba3a87
parent 7613 fe818734c387
child 7676 811022c3837e