src/Pure/Isar/outer_syntax.ML
changeset 13377 cc8245843abc
parent 12943 1db24da0537b
child 14091 ad6ba9c55190