--- a/src/HOL/Tools/typedef_package.ML Thu Jul 08 18:35:44 1999 +0200
+++ b/src/HOL/Tools/typedef_package.ML Thu Jul 08 18:36:09 1999 +0200
@@ -195,7 +195,7 @@
val goal = Thm.term_of (goal_nonempty cset);
in
thy
- |> IsarThy.theorem_i (("", [typedef_attribute cset do_typedef], (goal, [])), comment) int
+ |> IsarThy.theorem_i (("", [typedef_attribute cset do_typedef], (goal, ([], []))), comment) int
end;
val typedef_proof = gen_typedef_proof read_term;
--- 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;
--- a/src/Pure/Isar/skip_proof.ML Thu Jul 08 18:35:44 1999 +0200
+++ b/src/Pure/Isar/skip_proof.ML Thu Jul 08 18:36:09 1999 +0200
@@ -38,8 +38,8 @@
val thm = Thm.invoke_oracle thy skip_proofN (Theory.sign_of thy, SkipProof);
in Method.METHOD (fn _ => ALLGOALS (Tactic.rtac thm)) end;
-val local_skip_proof = Method.local_terminal_proof (Method.Basic cheat_meth);
-val global_skip_proof = Method.global_terminal_proof (Method.Basic cheat_meth);
+val local_skip_proof = Method.local_terminal_proof (Method.Basic cheat_meth, None);
+val global_skip_proof = Method.global_terminal_proof (Method.Basic cheat_meth, None);
(* proof command *)
--- a/src/Pure/axclass.ML Thu Jul 08 18:35:44 1999 +0200
+++ b/src/Pure/axclass.ML Thu Jul 08 18:36:09 1999 +0200
@@ -408,7 +408,7 @@
fun inst_proof mk_prop add_thms (sig_prop, comment) int thy =
thy
|> IsarThy.theorem_i (("", [inst_attribute add_thms],
- (mk_prop (Theory.sign_of thy) sig_prop, [])), comment) int;
+ (mk_prop (Theory.sign_of thy) sig_prop, ([], []))), comment) int;
val instance_subclass_proof = inst_proof (mk_classrel oo intrn_classrel) add_classrel_thms;
val instance_subclass_proof_i = inst_proof (K mk_classrel) add_classrel_thms;