--- 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);