src/Pure/Isar/outer_syntax.ML
changeset 74510 21a20b990724
parent 74262 839a6e284545
child 74561 8e6c973003c8