src/Pure/Isar/outer_syntax.ML
changeset 8919 d00b01ed8539
parent 8807 0046be1769f9
child 8999 ad8260dc6e4a