--- 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
--- 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 =