CONJUNCTS: full nesting (again), PRECISE_CONJUNCTS: outer level of nesting;
authorwenzelm
Fri Dec 23 15:16:49 2005 +0100 (2005-12-23)
changeset 185008b1a4e8ed199
parent 18499 567370efb6d7
child 18501 915105af2e80
CONJUNCTS: full nesting (again), PRECISE_CONJUNCTS: outer level of nesting;
src/Pure/tactic.ML
     1.1 --- a/src/Pure/tactic.ML	Fri Dec 23 15:16:48 2005 +0100
     1.2 +++ b/src/Pure/tactic.ML	Fri Dec 23 15:16:49 2005 +0100
     1.3 @@ -98,8 +98,8 @@
     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: int -> tactic -> int -> tactic
     1.8 -  val CONJUNCTS2: int -> tactic -> int -> tactic
     1.9 +  val CONJUNCTS: tactic -> int -> tactic
    1.10 +  val PRECISE_CONJUNCTS: int -> tactic -> int -> tactic
    1.11  end;
    1.12  
    1.13  signature TACTIC =
    1.14 @@ -650,15 +650,16 @@
    1.15        | tac n i = conj_tac i THEN TRY (fn st => tac (n - 1) (i + 1) st);
    1.16    in TRY oo tac end;
    1.17  
    1.18 -(*treat conjuncts as separate sub-goals*)
    1.19 -fun CONJUNCTS n tac =
    1.20 +fun CONJUNCTS tac =
    1.21 +  SELECT_GOAL (conjunction_tac 1
    1.22 +    THEN tac
    1.23 +    THEN PRIMITIVE Drule.conj_curry);
    1.24 +
    1.25 +fun PRECISE_CONJUNCTS n tac =
    1.26    SELECT_GOAL (precise_conjunction_tac n 1
    1.27      THEN tac
    1.28      THEN PRIMITIVE Drule.conj_curry);
    1.29  
    1.30 -(*treat two levels of conjunctions*)
    1.31 -fun CONJUNCTS2 n tac = CONJUNCTS n (ALLGOALS (CONJUNCTS ~1 tac));
    1.32 -
    1.33  end;
    1.34  
    1.35  structure BasicTactic: BASIC_TACTIC = Tactic;