src/Pure/Isar/isar_syn.ML

 
 (** proof commands **)
 
 (* 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"
     (statement IsarThy.theorem >> (fn f => Toplevel.print o Toplevel.theory_to_proof f));
 

 
 (* proof context *)
 
 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 =
   OuterSyntax.parser false "fix" "fix variables (Skolem constants)"
     (Scan.repeat1 (name -- Scan.option ($$$ "::" |-- typ))
       >> (fn xs => Toplevel.print o Toplevel.proof (IsarThy.fix xs)));
 
 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)));
 
 
 (* proof structure *)
 

 (*keep keywords consistent with the parsers, including those in
   outer_parse.ML, otherwise be prepared for unexpected errors*)
 
 val keywords =
  ["(", ")", "*", "+", ",", ":", "::", ";", "<", "<=", "=", "==", "=>",
-  "?", "[", "]", "and", "binder", "infixl", "infixr", "mixfix", "output",
-  "{", "|", "}"];
+  "?", "[", "]", "and", "as", "binder", "infixl", "infixr", "is",
+  "mixfix", "output", "{", "|", "}"];
 
 val parsers = [
   (*theory structure*)
   contextP, theoryP, endP,
   (*theory sections*)