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