# HG changeset patch
# User wenzelm
# Date 902392653 -7200
# Node ID 8862ed2db4317e63dfaa92b41b1eb67fdf499363
# Parent  212d203d6cd3778c19797d61b0467b1aad3e4fac
added solve_tac;

diff -r 212d203d6cd3 -r 8862ed2db431 src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Thu Aug 06 10:37:03 1998 +0200
+++ b/src/Pure/tactic.ML	Thu Aug 06 10:37:33 1998 +0200
@@ -82,6 +82,7 @@
   val rotate_tac	: int -> int -> tactic
   val rtac		: thm -> int -> tactic
   val rule_by_tactic	: tactic -> thm -> thm
+  val solve_tac		: thm list -> int -> tactic
   val subgoal_tac	: string -> int -> tactic
   val subgoals_tac	: string list -> int -> tactic
   val subgoals_of_brl	: bool * thm -> int
@@ -179,6 +180,8 @@
 (*Use an assumption or some rules ... A popular combination!*)
 fun ares_tac rules = assume_tac  ORELSE'  resolve_tac rules;
 
+fun solve_tac rules = resolve_tac rules THEN_ALL_NEW assume_tac;
+
 (*Matching tactics -- as above, but forbid updating of state*)
 fun bimatch_tac brules i = PRIMSEQ (biresolution true brules i);
 fun match_tac rules  = bimatch_tac (map (pair false) rules);