src/Pure/Isar/isar_syn.ML
changeset 6265 aaabe48bafcb
parent 6245 ebce4ebba491
child 6353 5a76eb9030df
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Mon Feb 08 17:33:03 1999 +0100
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Mon Feb 08 17:33:24 1999 +0100
     1.3 @@ -210,7 +210,7 @@
     1.4  (* use ML text *)
     1.5  
     1.6  val useP =
     1.7 -  OuterSyntax.parser true "use" "eval ML text from file"
     1.8 +  OuterSyntax.parser false "use" "eval ML text from file"
     1.9      (name >> IsarCmd.use);
    1.10  
    1.11  val mlP =
    1.12 @@ -511,7 +511,7 @@
    1.13  
    1.14  val keywords =
    1.15   ["(", ")", "*", "+", "--", ",", ":", "::", ";", "<", "<=", "=", "==", "=>",
    1.16 -  "?", "[", "]", "and", "as", "binder", "infixl", "infixr", "is",
    1.17 +  "?", "[", "]", "and", "as", "binder", "files", "infixl", "infixr", "is",
    1.18    "output", "{", "|", "}"];
    1.19  
    1.20  val parsers = [