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*)
```