# HG changeset patch
# User wenzelm
# Date 911472476 -3600
# Node ID a777d702e81fd8cb2d3cf246ec2133609a05592a
# Parent  406eb27fe53c558698a62692bf0423819b2393c4
let: 'as' patterns;
statements: propp ('is' patterns);

diff -r 406eb27fe53c -r a777d702e81f src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Thu Nov 19 11:47:22 1998 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Thu Nov 19 11:47:56 1998 +0100
@@ -246,7 +246,9 @@
 
 (* statements *)
 
-fun statement f = opt_thm_name ":" -- prop >> (fn ((x, y), z) => f x y z);
+val is_props = $$$ "(" |-- !!! (Scan.repeat1 ($$$ "is" |-- prop) --| $$$ ")");
+val propp = prop -- Scan.optional is_props [];
+fun statement f = opt_thm_name ":" -- propp >> (fn ((x, y), z) => f x y z);
 
 val theoremP =
   OuterSyntax.parser false "theorem" "state theorem"
@@ -284,7 +286,7 @@
 
 val assumeP =
   OuterSyntax.parser false "assume" "assume propositions"
-    (opt_thm_name ":" -- Scan.repeat1 prop >>
+    (opt_thm_name ":" -- Scan.repeat1 propp >>
       (fn ((x, y), z) => Toplevel.print o Toplevel.proof (IsarThy.assume x y z)));
 
 val fixP =
@@ -294,7 +296,7 @@
 
 val letP =
   OuterSyntax.parser false "let" "bind text variables"
-    (enum1 "and" (term -- ($$$ "=" |-- term))
+    (enum1 "and" (enum1 "as" term -- ($$$ "=" |-- term))
       >> (fn bs => Toplevel.print o Toplevel.proof (IsarThy.match_bind bs)));
 
 
@@ -482,8 +484,8 @@
 
 val keywords =
  ["(", ")", "*", "+", ",", ":", "::", ";", "<", "<=", "=", "==", "=>",
-  "?", "[", "]", "and", "binder", "infixl", "infixr", "mixfix", "output",
-  "{", "|", "}"];
+  "?", "[", "]", "and", "as", "binder", "infixl", "infixr", "is",
+  "mixfix", "output", "{", "|", "}"];
 
 val parsers = [
   (*theory structure*)