added solve_tac;
authorwenzelm
Thu Aug 06 10:37:33 1998 +0200 (1998-08-06)
changeset 52638862ed2db431
parent 5262 212d203d6cd3
child 5264 7538fce1fe37
added solve_tac;
src/Pure/tactic.ML
     1.1 --- a/src/Pure/tactic.ML	Thu Aug 06 10:37:03 1998 +0200
     1.2 +++ b/src/Pure/tactic.ML	Thu Aug 06 10:37:33 1998 +0200
     1.3 @@ -82,6 +82,7 @@
     1.4    val rotate_tac	: int -> int -> tactic
     1.5    val rtac		: thm -> int -> tactic
     1.6    val rule_by_tactic	: tactic -> thm -> thm
     1.7 +  val solve_tac		: thm list -> int -> tactic
     1.8    val subgoal_tac	: string -> int -> tactic
     1.9    val subgoals_tac	: string list -> int -> tactic
    1.10    val subgoals_of_brl	: bool * thm -> int
    1.11 @@ -179,6 +180,8 @@
    1.12  (*Use an assumption or some rules ... A popular combination!*)
    1.13  fun ares_tac rules = assume_tac  ORELSE'  resolve_tac rules;
    1.14  
    1.15 +fun solve_tac rules = resolve_tac rules THEN_ALL_NEW assume_tac;
    1.16 +
    1.17  (*Matching tactics -- as above, but forbid updating of state*)
    1.18  fun bimatch_tac brules i = PRIMSEQ (biresolution true brules i);
    1.19  fun match_tac rules  = bimatch_tac (map (pair false) rules);