--- a/src/Pure/Isar/isar_syn.ML Wed Apr 05 21:01:33 2000 +0200
+++ b/src/Pure/Isar/isar_syn.ML Wed Apr 05 21:01:59 2000 +0200
@@ -332,7 +332,7 @@
val letP =
OuterSyntax.command "let" "bind text variables" K.prf_decl
- (P.and_list1 (P.enum1 "as" P.term -- (P.$$$ "=" |-- P.term) -- P.marg_comment)
+ (P.and_list1 (P.enum1 "and" P.term -- (P.$$$ "=" |-- P.term) -- P.marg_comment)
>> (Toplevel.print oo (Toplevel.proof o IsarThy.let_bind)));
val caseP =
@@ -624,9 +624,8 @@
val keywords =
["!", "!!", "%", "%%", "(", ")", "+", ",", "--", ":", "::", ";", "<",
- "<=", "=", "==", "=>", "?", "[", "]", "and", "as", "binder",
- "concl", "files", "in", "infixl", "infixr", "is", "output", "{",
- "|", "}"];
+ "<=", "=", "==", "=>", "?", "[", "]", "and", "binder", "concl",
+ "files", "in", "infixl", "infixr", "is", "output", "{", "|", "}"];
val parsers = [
(*theory structure*)