src/Pure/Isar/isar_syn.ML
changeset 5937 a777d702e81f
parent 5924 b9d5f5901b59
child 5944 dcc446da8e19
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Thu Nov 19 11:47:22 1998 +0100
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Thu Nov 19 11:47:56 1998 +0100
     1.3 @@ -246,7 +246,9 @@
     1.4  
     1.5  (* statements *)
     1.6  
     1.7 -fun statement f = opt_thm_name ":" -- prop >> (fn ((x, y), z) => f x y z);
     1.8 +val is_props = $$$ "(" |-- !!! (Scan.repeat1 ($$$ "is" |-- prop) --| $$$ ")");
     1.9 +val propp = prop -- Scan.optional is_props [];
    1.10 +fun statement f = opt_thm_name ":" -- propp >> (fn ((x, y), z) => f x y z);
    1.11  
    1.12  val theoremP =
    1.13    OuterSyntax.parser false "theorem" "state theorem"
    1.14 @@ -284,7 +286,7 @@
    1.15  
    1.16  val assumeP =
    1.17    OuterSyntax.parser false "assume" "assume propositions"
    1.18 -    (opt_thm_name ":" -- Scan.repeat1 prop >>
    1.19 +    (opt_thm_name ":" -- Scan.repeat1 propp >>
    1.20        (fn ((x, y), z) => Toplevel.print o Toplevel.proof (IsarThy.assume x y z)));
    1.21  
    1.22  val fixP =
    1.23 @@ -294,7 +296,7 @@
    1.24  
    1.25  val letP =
    1.26    OuterSyntax.parser false "let" "bind text variables"
    1.27 -    (enum1 "and" (term -- ($$$ "=" |-- term))
    1.28 +    (enum1 "and" (enum1 "as" term -- ($$$ "=" |-- term))
    1.29        >> (fn bs => Toplevel.print o Toplevel.proof (IsarThy.match_bind bs)));
    1.30  
    1.31  
    1.32 @@ -482,8 +484,8 @@
    1.33  
    1.34  val keywords =
    1.35   ["(", ")", "*", "+", ",", ":", "::", ";", "<", "<=", "=", "==", "=>",
    1.36 -  "?", "[", "]", "and", "binder", "infixl", "infixr", "mixfix", "output",
    1.37 -  "{", "|", "}"];
    1.38 +  "?", "[", "]", "and", "as", "binder", "infixl", "infixr", "is",
    1.39 +  "mixfix", "output", "{", "|", "}"];
    1.40  
    1.41  val parsers = [
    1.42    (*theory structure*)