src/Pure/Isar/outer_syntax.ML
changeset 72724 75cce7926ec1
parent 72434 cc27cf7e51c6
child 73098 8a20737e4ebf