added CONJUNCTS: treat conjunction as separate sub-goals;

--- a/src/Pure/tactic.ML	Sat Nov 19 14:21:05 2005 +0100
+++ b/src/Pure/tactic.ML	Sat Nov 19 14:21:06 2005 +0100
@@ -98,6 +98,7 @@
   val instantiate_tac   : (string * string) list -> tactic
   val thin_tac          : string -> int -> tactic
   val trace_goalno_tac  : (int -> tactic) -> int -> tactic
+  val CONJUNCTS: tactic -> int -> tactic
 end;
 
 signature TACTIC =
@@ -644,6 +645,12 @@
 fun smart_conjunction_tac 0 = assume_tac 1
   | smart_conjunction_tac _ = TRY conjunction_tac;
 
+(*treat conjunction as separate sub-goals*)
+fun CONJUNCTS tac =
+  SELECT_GOAL (TRY conjunction_tac
+    THEN tac
+    THEN PRIMITIVE Drule.conj_curry);
+
 end;
 
 structure BasicTactic: BASIC_TACTIC = Tactic;