diff -r 059caec54d91 -r a6431098a929 src/Pure/tactic.ML
--- a/src/Pure/tactic.ML Wed Jun 08 15:14:09 2005 +0200
+++ b/src/Pure/tactic.ML Wed Jun 08 16:11:09 2005 +0200
@@ -111,10 +111,13 @@
val simplify: bool -> thm list -> thm -> thm
val conjunction_tac: tactic
val smart_conjunction_tac: int -> tactic
+ val prove_multi_plain: Sign.sg -> string list -> term list -> term list ->
+ (thm list -> tactic) -> thm list
val prove_multi: Sign.sg -> string list -> term list -> term list ->
(thm list -> tactic) -> thm list
val prove_multi_standard: Sign.sg -> string list -> term list -> term list ->
(thm list -> tactic) -> thm list
+ val prove_plain: Sign.sg -> string list -> term list -> term -> (thm list -> tactic) -> thm
val prove: Sign.sg -> string list -> term list -> term -> (thm list -> tactic) -> thm
val prove_standard: Sign.sg -> string list -> term list -> term ->
(thm list -> tactic) -> thm
@@ -659,7 +662,7 @@
(** minimal goal interface for programmed proofs *)
-fun prove_multi sign xs asms props tac =
+fun gen_prove_multi finish_thm sign xs asms props tac =
let
val prop = Logic.mk_conjunction_list props;
val statement = Logic.list_implies (asms, prop);
@@ -700,14 +703,19 @@
|> map (fn res => res
|> Drule.implies_intr_list casms
|> Drule.forall_intr_list cparams
- |> norm_hhf_rule
- |> (#1 o Thm.varifyT' fixed_tfrees)
- |> Drule.zero_var_indexes)
+ |> finish_thm fixed_tfrees)
end;
+fun prove_multi_plain sign xs asms prop tac =
+ gen_prove_multi (K norm_hhf_plain) sign xs asms prop tac;
+fun prove_multi sign xs asms prop tac =
+ gen_prove_multi (fn fixed_tfrees => Drule.zero_var_indexes o
+ (#1 o Thm.varifyT' fixed_tfrees) o norm_hhf_rule)
+ sign xs asms prop tac;
fun prove_multi_standard sign xs asms prop tac =
map Drule.standard (prove_multi sign xs asms prop tac);
+fun prove_plain sign xs asms prop tac = hd (prove_multi_plain sign xs asms [prop] tac);
fun prove sign xs asms prop tac = hd (prove_multi sign xs asms [prop] tac);
fun prove_standard sign xs asms prop tac = Drule.standard (prove sign xs asms prop tac);