src/Pure/Isar/isar_syn.ML
changeset 27353 71c4dd53d4cb
parent 27200 00b7b55b61bd
child 27378 0968c0d0b969
equal deleted inserted replaced
27352:8adeff7fd4bc 27353:71c4dd53d4cb
    14 (** keywords **)
    14 (** keywords **)
    15 
    15 
    16 (*keep keywords consistent with the parsers, otherwise be prepared for
    16 (*keep keywords consistent with the parsers, otherwise be prepared for
    17   unexpected errors*)
    17   unexpected errors*)
    18 
    18 
    19 val _ = OuterSyntax.keywords
    19 val _ = List.app OuterKeyword.keyword
    20  ["!!", "!", "%", "(", ")", "+", ",", "--", ":", "::", ";", "<", "<=",
    20  ["!!", "!", "%", "(", ")", "+", ",", "--", ":", "::", ";", "<", "<=",
    21   "=", "==", "=>", "?", "[", "\\<equiv>", "\\<leftharpoondown>",
    21   "=", "==", "=>", "?", "[", "\\<equiv>", "\\<leftharpoondown>",
    22   "\\<rightharpoonup>", "\\<rightleftharpoons>", "\\<subseteq>", "]",
    22   "\\<rightharpoonup>", "\\<rightleftharpoons>", "\\<subseteq>", "]",
    23   "advanced", "and", "assumes", "attach", "begin", "binder",
    23   "advanced", "and", "assumes", "attach", "begin", "binder",
    24   "constrains", "defines", "fixes", "for", "identifier", "if",
    24   "constrains", "defines", "fixes", "for", "identifier", "if",