# HG changeset patch
# User oheimb
# Date 909167699 -7200
# Node ID 98744e38ded1a03f693534a925b3b8e1317a908e
# Parent  c90b5f7d0c613025d49bea5c83b9105b3fffe0df
added SOLVE tactical

diff -r c90b5f7d0c61 -r 98744e38ded1 doc-src/Ref/tctical.tex
--- a/doc-src/Ref/tctical.tex	Fri Oct 23 20:28:33 1998 +0200
+++ b/doc-src/Ref/tctical.tex	Fri Oct 23 20:34:59 1998 +0200
@@ -254,6 +254,7 @@
 \begin{ttbox} 
 COND        : (thm->bool) -> tactic -> tactic -> tactic
 IF_UNSOLVED : tactic -> tactic
+SOLVE       : tactic -> tactic
 DETERM      : tactic -> tactic
 \end{ttbox}
 \begin{ttdescription}
@@ -268,6 +269,10 @@
 returns the proof state otherwise.  Many common tactics, such as {\tt
 resolve_tac}, fail if applied to a proof state that has no subgoals.
 
+\item[\ttindexbold{SOLVE} {\it tac}] 
+applies {\it tac\/} to the proof state and then fails iff there are subgoals
+left.
+
 \item[\ttindexbold{DETERM} {\it tac}] 
 applies {\it tac\/} to the proof state and returns the head of the
 resulting sequence.  {\tt DETERM} limits the search space by making its
diff -r c90b5f7d0c61 -r 98744e38ded1 src/Pure/search.ML
--- a/src/Pure/search.ML	Fri Oct 23 20:28:33 1998 +0200
+++ b/src/Pure/search.ML	Fri Oct 23 20:34:59 1998 +0200
@@ -23,6 +23,7 @@
 
   val has_fewer_prems	: int -> thm -> bool   
   val IF_UNSOLVED	: tactic -> tactic
+  val SOLVE		: tactic -> tactic
   val trace_BEST_FIRST	: bool ref
   val BEST_FIRST	: (thm -> bool) * (thm -> int) -> tactic -> tactic
   val THEN_BEST_FIRST	: tactic -> (thm->bool) * (thm->int) -> tactic
@@ -65,6 +66,9 @@
 (*Apply a tactic if subgoals remain, else do nothing.*)
 val IF_UNSOLVED = COND (has_fewer_prems 1) all_tac;
 
+(*Force a tactic to solve its goal completely, otherwise fail *)
+fun SOLVE tac = tac THEN COND (has_fewer_prems 1) all_tac no_tac;
+
 (*Execute tac1, but only execute tac2 if there are at least as many subgoals
   as before.  This ensures that tac2 is only applied to an outcome of tac1.*)
 fun (tac1 THEN_MAYBE tac2) st =