removed "as" keyword;
authorwenzelm
Wed Apr 05 21:01:59 2000 +0200 (2000-04-05)
changeset 86693ccb29fb26ef
parent 8668 ee73e7b26686
child 8670 d69616c74211
removed "as" keyword;
src/Pure/Isar/isar_syn.ML
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Wed Apr 05 21:01:33 2000 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Wed Apr 05 21:01:59 2000 +0200
     1.3 @@ -332,7 +332,7 @@
     1.4  
     1.5  val letP =
     1.6    OuterSyntax.command "let" "bind text variables" K.prf_decl
     1.7 -    (P.and_list1 (P.enum1 "as" P.term -- (P.$$$ "=" |-- P.term) -- P.marg_comment)
     1.8 +    (P.and_list1 (P.enum1 "and" P.term -- (P.$$$ "=" |-- P.term) -- P.marg_comment)
     1.9        >> (Toplevel.print oo (Toplevel.proof o IsarThy.let_bind)));
    1.10  
    1.11  val caseP =
    1.12 @@ -624,9 +624,8 @@
    1.13  
    1.14  val keywords =
    1.15   ["!", "!!", "%", "%%", "(", ")", "+", ",", "--", ":", "::", ";", "<",
    1.16 -  "<=", "=", "==", "=>", "?", "[", "]", "and", "as", "binder",
    1.17 -  "concl", "files", "in", "infixl", "infixr", "is", "output", "{",
    1.18 -  "|", "}"];
    1.19 +  "<=", "=", "==", "=>", "?", "[", "]", "and", "binder", "concl",
    1.20 +  "files", "in", "infixl", "infixr", "is", "output", "{", "|", "}"];
    1.21  
    1.22  val parsers = [
    1.23    (*theory structure*)