# HG changeset patch
# User wenzelm
# Date 1132406466 -3600
# Node ID 6bcd9b2ca49b662d5a9839a0819911d2766d89a2
# Parent  dbdcf366db53ab054cfaead2b08d11523c69d4c0
added CONJUNCTS: treat conjunction as separate sub-goals;

diff -r dbdcf366db53 -r 6bcd9b2ca49b src/Pure/tactic.ML
--- 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;