# HG changeset patch
# User wenzelm
# Date 1005510712 -3600
# Node ID d51d50636332f27ad14fa357f0895fc24e79bde1
# Parent  7cad58fbc866fe35e40e9da8a4a977caf8267ab2
added conjunction_tac;

diff -r 7cad58fbc866 -r d51d50636332 src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Sun Nov 11 21:31:35 2001 +0100
+++ b/src/Pure/tactic.ML	Sun Nov 11 21:31:52 2001 +0100
@@ -112,6 +112,7 @@
   val rewrite: bool -> thm list -> cterm -> thm
   val rewrite_cterm: bool -> thm list -> cterm -> cterm
   val simplify: bool -> thm list -> thm -> thm
+  val conjunction_tac: tactic
   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
 end;
@@ -610,6 +611,17 @@
   end;
 
 
+(*meta-level conjunction*)
+val conj_tac = SUBGOAL (fn (Const ("all", _) $ Abs (_, _, Const ("==>", _) $
+      (Const ("==>", _) $ _ $ (Const ("==>", _) $ _ $ Bound 0)) $ Bound 0), i) =>
+    (fn st =>
+      compose_tac (false, Drule.incr_indexes_wrt [] [] [] [st] Drule.conj_intr_thm, 2) i st)
+  | _ => no_tac);
+  
+val conjunction_tac = ALLGOALS (REPEAT_ALL_NEW conj_tac);
+
+
+
 (** minimal goal interface for internal use *)
 
 fun prove sign xs asms prop tac =