--- a/src/Pure/Isar/outer_parse.ML Thu Jul 08 18:35:44 1999 +0200
+++ b/src/Pure/Isar/outer_parse.ML Thu Jul 08 18:36:09 1999 +0200
@@ -49,6 +49,7 @@
val const: token list -> (bstring * string * Syntax.mixfix) * token list
val term: token list -> string * token list
val prop: token list -> string * token list
+ val propp: token list -> (string * (string list * string list)) * token list
val attribs: token list -> Args.src list * token list
val opt_attribs: token list -> Args.src list * token list
val thm_name: string -> token list -> (bstring * Args.src list) * token list
@@ -223,6 +224,15 @@
val prop = group "proposition" trm;
+(* prop patters *)
+
+val is_props = Scan.repeat1 ($$$ "is" |-- prop);
+val concl_props = $$$ "concl" |-- !!! is_props;
+val any_props = is_props -- Scan.optional concl_props [] || concl_props >> pair [];
+
+val propp = prop -- Scan.optional ($$$ "(" |-- !!! (any_props --| $$$ ")")) ([], []);
+
+
(* arguments *)
val keyword_symid = Scan.one (OuterLex.keyword_pred OuterLex.is_sid) >> OuterLex.val_of;