diff -r 02d9f110ecc1 -r 6236cc88d4b8 src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Thu Apr 28 17:57:13 2005 +0200
+++ b/src/Pure/tactic.ML	Thu Apr 28 21:35:25 2005 +0200
@@ -110,8 +110,14 @@
   val rewrite: bool -> thm list -> cterm -> thm
   val simplify: bool -> thm list -> thm -> thm
   val conjunction_tac: tactic
+  val smart_conjunction_tac: int -> tactic
+  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: 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
+  val prove_standard: Sign.sg -> string list -> term list -> term ->
+    (thm list -> tactic) -> thm
   val compose_inst_tac' : (indexname * string) list -> (bool * thm * int) ->
                           int -> tactic
   val lift_inst_rule'   : thm * int * (indexname * string) list * thm -> thm
@@ -641,12 +647,16 @@
   
 val conjunction_tac = ALLGOALS (REPEAT_ALL_NEW conj_tac);
 
+fun smart_conjunction_tac 0 = assume_tac 1
+  | smart_conjunction_tac _ = TRY conjunction_tac;
+
 
 
-(** minimal goal interface for internal use *)
+(** minimal goal interface for programmed proofs *)
 
-fun prove sign xs asms prop tac =
+fun prove_multi sign xs asms props tac =
   let
+    val prop = Logic.mk_conjunction_list props;
     val statement = Logic.list_implies (asms, prop);
     val frees = map Term.dest_Free (Term.term_frees statement);
     val fixed_frees = filter_out (fn (x, _) => x mem_string xs) frees;
@@ -671,23 +681,29 @@
     val goal' =
       (case Seq.pull (tac prems goal) of SOME (goal', _) => goal' | _ => err "Tactic failed.");
     val ngoals = Thm.nprems_of goal';
+    val _ = conditional (ngoals <> 0) (fn () =>
+      err ("Proof failed.\n" ^
+        Pretty.string_of (Pretty.chunks (Display.pretty_goals ngoals goal')) ^
+        ("\n" ^ string_of_int ngoals ^ " unsolved goal(s)!")));
+
     val raw_result = goal' RS Drule.rev_triv_goal;
     val prop' = prop_of raw_result;
+    val _ = conditional (not (Pattern.matches (Sign.tsig_of sign) (prop, prop'))) (fn () =>
+      err ("Proved a different theorem: " ^ Sign.string_of_term sign prop'));
   in
-    if ngoals <> 0 then
-      err ("Proof failed.\n" ^ Pretty.string_of (Pretty.chunks (Display.pretty_goals ngoals goal'))
-        ^ ("\n" ^ string_of_int ngoals ^ " unsolved goal(s)!"))
-    else if not (Pattern.matches (Sign.tsig_of sign) (prop, prop')) then
-      err ("Proved a different theorem: " ^ Sign.string_of_term sign prop')
-    else
-      raw_result
+    Drule.conj_elim_precise (length props) raw_result
+    |> 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
+      |> Drule.zero_var_indexes)
   end;
 
+fun prove_multi_standard sign xs asms prop tac =
+  map Drule.standard (prove_multi 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);
 
 end;