src/Pure/Isar/outer_syntax.ML
changeset 8352 0fda5ba36934
parent 8209 4816ba139574
child 8583 34c4847fd8c1