added CONJUNCTS: treat conjunction as separate sub-goals;
authorwenzelm
Sat Nov 19 14:21:06 2005 +0100 (2005-11-19)
changeset 182096bcd9b2ca49b
parent 18208 dbdcf366db53
child 18210 ad4b8567f6eb
added CONJUNCTS: treat conjunction as separate sub-goals;
src/Pure/tactic.ML
     1.1 --- a/src/Pure/tactic.ML	Sat Nov 19 14:21:05 2005 +0100
     1.2 +++ b/src/Pure/tactic.ML	Sat Nov 19 14:21:06 2005 +0100
     1.3 @@ -98,6 +98,7 @@
     1.4    val instantiate_tac   : (string * string) list -> tactic
     1.5    val thin_tac          : string -> int -> tactic
     1.6    val trace_goalno_tac  : (int -> tactic) -> int -> tactic
     1.7 +  val CONJUNCTS: tactic -> int -> tactic
     1.8  end;
     1.9  
    1.10  signature TACTIC =
    1.11 @@ -644,6 +645,12 @@
    1.12  fun smart_conjunction_tac 0 = assume_tac 1
    1.13    | smart_conjunction_tac _ = TRY conjunction_tac;
    1.14  
    1.15 +(*treat conjunction as separate sub-goals*)
    1.16 +fun CONJUNCTS tac =
    1.17 +  SELECT_GOAL (TRY conjunction_tac
    1.18 +    THEN tac
    1.19 +    THEN PRIMITIVE Drule.conj_curry);
    1.20 +
    1.21  end;
    1.22  
    1.23  structure BasicTactic: BASIC_TACTIC = Tactic;