added conjunction_tac;
authorwenzelm
Sun Nov 11 21:31:52 2001 +0100 (2001-11-11)
changeset 12139d51d50636332
parent 12138 7cad58fbc866
child 12140 a987beab002d
added conjunction_tac;
src/Pure/tactic.ML
     1.1 --- a/src/Pure/tactic.ML	Sun Nov 11 21:31:35 2001 +0100
     1.2 +++ b/src/Pure/tactic.ML	Sun Nov 11 21:31:52 2001 +0100
     1.3 @@ -112,6 +112,7 @@
     1.4    val rewrite: bool -> thm list -> cterm -> thm
     1.5    val rewrite_cterm: bool -> thm list -> cterm -> cterm
     1.6    val simplify: bool -> thm list -> thm -> thm
     1.7 +  val conjunction_tac: tactic
     1.8    val prove: Sign.sg -> string list -> term list -> term -> (thm list -> tactic) -> thm
     1.9    val prove_standard: Sign.sg -> string list -> term list -> term -> (thm list -> tactic) -> thm
    1.10  end;
    1.11 @@ -610,6 +611,17 @@
    1.12    end;
    1.13  
    1.14  
    1.15 +(*meta-level conjunction*)
    1.16 +val conj_tac = SUBGOAL (fn (Const ("all", _) $ Abs (_, _, Const ("==>", _) $
    1.17 +      (Const ("==>", _) $ _ $ (Const ("==>", _) $ _ $ Bound 0)) $ Bound 0), i) =>
    1.18 +    (fn st =>
    1.19 +      compose_tac (false, Drule.incr_indexes_wrt [] [] [] [st] Drule.conj_intr_thm, 2) i st)
    1.20 +  | _ => no_tac);
    1.21 +  
    1.22 +val conjunction_tac = ALLGOALS (REPEAT_ALL_NEW conj_tac);
    1.23 +
    1.24 +
    1.25 +
    1.26  (** minimal goal interface for internal use *)
    1.27  
    1.28  fun prove sign xs asms prop tac =