src/Pure/Isar/outer_syntax.ML
changeset 72520 581d9d74e1e4
parent 72434 cc27cf7e51c6
child 73098 8a20737e4ebf
equal deleted inserted replaced
72519:f760554a5a29 72520:581d9d74e1e4