1.1 --- a/doc-src/Ref/tctical.tex Fri Oct 23 20:28:33 1998 +0200
1.2 +++ b/doc-src/Ref/tctical.tex Fri Oct 23 20:34:59 1998 +0200
1.3 @@ -254,6 +254,7 @@
1.4 \begin{ttbox}
1.5 COND : (thm->bool) -> tactic -> tactic -> tactic
1.6 IF_UNSOLVED : tactic -> tactic
1.7 +SOLVE : tactic -> tactic
1.8 DETERM : tactic -> tactic
1.9 \end{ttbox}
1.10 \begin{ttdescription}
1.11 @@ -268,6 +269,10 @@
1.12 returns the proof state otherwise. Many common tactics, such as {\tt
1.13 resolve_tac}, fail if applied to a proof state that has no subgoals.
1.14
1.15 +\item[\ttindexbold{SOLVE} {\it tac}]
1.16 +applies {\it tac\/} to the proof state and then fails iff there are subgoals
1.17 +left.
1.18 +
1.19 \item[\ttindexbold{DETERM} {\it tac}]
1.20 applies {\it tac\/} to the proof state and returns the head of the
1.21 resulting sequence. {\tt DETERM} limits the search space by making its

2.1 --- a/src/Pure/search.ML Fri Oct 23 20:28:33 1998 +0200
2.2 +++ b/src/Pure/search.ML Fri Oct 23 20:34:59 1998 +0200
2.3 @@ -23,6 +23,7 @@
2.4
2.5 val has_fewer_prems : int -> thm -> bool
2.6 val IF_UNSOLVED : tactic -> tactic
2.7 + val SOLVE : tactic -> tactic
2.8 val trace_BEST_FIRST : bool ref
2.9 val BEST_FIRST : (thm -> bool) * (thm -> int) -> tactic -> tactic
2.10 val THEN_BEST_FIRST : tactic -> (thm->bool) * (thm->int) -> tactic
2.11 @@ -65,6 +66,9 @@
2.12 (*Apply a tactic if subgoals remain, else do nothing.*)
2.13 val IF_UNSOLVED = COND (has_fewer_prems 1) all_tac;
2.14
2.15 +(*Force a tactic to solve its goal completely, otherwise fail *)
2.16 +fun SOLVE tac = tac THEN COND (has_fewer_prems 1) all_tac no_tac;
2.17 +
2.18 (*Execute tac1, but only execute tac2 if there are at least as many subgoals
2.19 as before. This ensures that tac2 is only applied to an outcome of tac1.*)
2.20 fun (tac1 THEN_MAYBE tac2) st =