and_list;
authorwenzelm
Thu Dec 03 14:10:04 1998 +0100 (1998-12-03 ago)
changeset 60136da9ae6d40f5
parent 6012 1894bfc4aee9
child 6014 bfd4923b0957
and_list;
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/outer_parse.ML
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Thu Dec 03 10:45:06 1998 +0100
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Thu Dec 03 14:10:04 1998 +0100
     1.3 @@ -297,17 +297,17 @@
     1.4  
     1.5  val assumeP =
     1.6    OuterSyntax.parser false "assume" "assume propositions"
     1.7 -    (opt_thm_name ":" -- Scan.repeat1 propp >>
     1.8 +    (opt_thm_name ":" -- and_list1 propp >>
     1.9        (fn ((x, y), z) => Toplevel.print o Toplevel.proof (IsarThy.assume x y z)));
    1.10  
    1.11  val fixP =
    1.12    OuterSyntax.parser false "fix" "fix variables (Skolem constants)"
    1.13 -    (Scan.repeat1 (name -- Scan.option ($$$ "::" |-- typ))
    1.14 +    (and_list1 (name -- Scan.option ($$$ "::" |-- typ))
    1.15        >> (fn xs => Toplevel.print o Toplevel.proof (IsarThy.fix xs)));
    1.16  
    1.17  val letP =
    1.18    OuterSyntax.parser false "let" "bind text variables"
    1.19 -    (enum1 "and" (enum1 "as" term -- ($$$ "=" |-- term))
    1.20 +    (and_list1 (enum1 "as" term -- ($$$ "=" |-- term))
    1.21        >> (fn bs => Toplevel.print o Toplevel.proof (IsarThy.match_bind bs)));
    1.22  
    1.23  
    1.24 @@ -508,7 +508,7 @@
    1.25  val keywords =
    1.26   ["(", ")", "*", "+", "--", ",", ":", "::", ";", "<", "<=", "=", "==", "=>",
    1.27    "?", "[", "]", "and", "as", "binder", "infixl", "infixr", "is",
    1.28 -  "mixfix", "output", "{", "|", "}"];
    1.29 +  "output", "{", "|", "}"];
    1.30  
    1.31  val parsers = [
    1.32    (*theory structure*)
     2.1 --- a/src/Pure/Isar/outer_parse.ML	Thu Dec 03 10:45:06 1998 +0100
     2.2 +++ b/src/Pure/Isar/outer_parse.ML	Thu Dec 03 14:10:04 1998 +0100
     2.3 @@ -30,6 +30,8 @@
     2.4    val enum1: string -> (token list -> 'a * token list) -> token list -> 'a list * token list
     2.5    val list: (token list -> 'a * token list) -> token list -> 'a list * token list
     2.6    val list1: (token list -> 'a * token list) -> token list -> 'a list * token list
     2.7 +  val and_list: (token list -> 'a * token list) -> token list -> 'a list * token list
     2.8 +  val and_list1: (token list -> 'a * token list) -> token list -> 'a list * token list
     2.9    val name: token list -> bstring * token list
    2.10    val xname: token list -> xstring * token list
    2.11    val text: token list -> string * token list
    2.12 @@ -133,6 +135,9 @@
    2.13  fun list1 scan = enum1 "," scan;
    2.14  fun list scan = enum "," scan;
    2.15  
    2.16 +fun and_list1 scan = enum1 "and" scan;
    2.17 +fun and_list scan = enum "and" scan;
    2.18 +
    2.19  
    2.20  (* names and text *)
    2.21  
    2.22 @@ -234,7 +239,7 @@
    2.23  fun opt_thm_name s = Scan.optional (thm_name s) ("", []);
    2.24  
    2.25  val xthm = xname -- opt_attribs;
    2.26 -val xthms1 = Scan.repeat1 xthm;
    2.27 +val xthms1 = and_list1 xthm;
    2.28  
    2.29  
    2.30  (* proof methods *)