src/Pure/Isar/outer_syntax.ML
changeset 39051 45facd8f358e
parent 38422 f96394dba335
child 40523 1050315f6ee2