updated "Control and search tacticals" (moved from ref to implementation);
discontinued odd trace flags that assume sequential TTY loop;
discontinued obscure DETERM_UNTIL_SOLVED;
discontinued obsolete chapter "Tacticals" (ref);

--- a/doc-src/IsarImplementation/Thy/Tactic.thy	Thu Jan 26 21:25:18 2012 +0100
+++ b/doc-src/IsarImplementation/Thy/Tactic.thy	Thu Jan 26 22:16:45 2012 +0100
@@ -404,9 +404,7 @@
   sequential composition, disjunctive choice, iteration, or goal
   addressing.  Various search strategies may be expressed via
   tacticals.
-
-  \medskip The chapter on tacticals in old \cite{isabelle-ref} is
-  still applicable for further details.  *}
+*}
 
 
 subsection {* Combining tactics *}
@@ -438,13 +436,13 @@
   \begin{description}
 
   \item @{text "tac\<^sub>1"}~@{ML_op THEN}~@{text "tac\<^sub>2"} is the sequential
-  composition of @{text "tac\<^sub>1"} and @{text "tac\<^sub>2"}.  Applied to a
-  proof state, it returns all states reachable in two steps by
-  applying @{text "tac\<^sub>1"} followed by @{text "tac\<^sub>2"}.  First, it
-  applies @{text "tac\<^sub>1"} to the proof state, getting a sequence of
-  possible next states; then, it applies @{text "tac\<^sub>2"} to each of
-  these and concatenates the results to produce again one flat
-  sequence of states.
+  composition of @{text "tac\<^sub>1"} and @{text "tac\<^sub>2"}.  Applied to a goal
+  state, it returns all states reachable in two steps by applying
+  @{text "tac\<^sub>1"} followed by @{text "tac\<^sub>2"}.  First, it applies @{text
+  "tac\<^sub>1"} to the goal state, getting a sequence of possible next
+  states; then, it applies @{text "tac\<^sub>2"} to each of these and
+  concatenates the results to produce again one flat sequence of
+  states.
 
   \item @{text "tac\<^sub>1"}~@{ML_op ORELSE}~@{text "tac\<^sub>2"} makes a choice
   between @{text "tac\<^sub>1"} and @{text "tac\<^sub>2"}.  Applied to a state, it
@@ -497,7 +495,7 @@
 
   \begin{description}
 
-  \item @{ML TRY}~@{text "tac"} applies @{text "tac"} to the proof
+  \item @{ML TRY}~@{text "tac"} applies @{text "tac"} to the goal
   state and returns the resulting sequence, if non-empty; otherwise it
   returns the original state.  Thus, it applies @{text "tac"} at most
   once.
@@ -506,7 +504,7 @@
   applied via functional composition: @{ML "TRY"}~@{ML_op o}~@{text
   "tac"}.  There is no need for @{verbatim TRY'}.
 
-  \item @{ML REPEAT}~@{text "tac"} applies @{text "tac"} to the proof
+  \item @{ML REPEAT}~@{text "tac"} applies @{text "tac"} to the goal
   state and, recursively, to each element of the resulting sequence.
   The resulting sequence consists of those states that make @{text
   "tac"} fail.  Thus, it applies @{text "tac"} as many times as
@@ -519,7 +517,7 @@
   is impossible.
 
   \item @{ML REPEAT_DETERM}~@{text "tac"} applies @{text "tac"} to the
-  proof state and, recursively, to the head of the resulting sequence.
+  goal state and, recursively, to the head of the resulting sequence.
   It returns the first state to make @{text "tac"} fail.  It is
   deterministic, discarding alternative outcomes.
 
@@ -561,7 +559,7 @@
   possible in each outcome.
 
   \begin{warn}
-  Note the explicit abstraction over the proof state in the ML
+  Note the explicit abstraction over the goal state in the ML
   definition of @{ML REPEAT}.  Recursive tacticals must be coded in
   this awkward fashion to avoid infinite recursion of eager functional
   evaluation in Standard ML.  The following attempt would make @{ML
@@ -632,4 +630,177 @@
   \end{description}
 *}
 
+
+subsection {* Control and search tacticals *}
+
+text {* A predicate on theorems @{ML_type "thm -> bool"} can test
+  whether a goal state enjoys some desirable property --- such as
+  having no subgoals.  Tactics that search for satisfactory goal
+  states are easy to express.  The main search procedures,
+  depth-first, breadth-first and best-first, are provided as
+  tacticals.  They generate the search tree by repeatedly applying a
+  given tactic.  *}
+
+
+subsubsection {* Filtering a tactic's results *}
+
+text {*
+  \begin{mldecls}
+  @{index_ML FILTER: "(thm -> bool) -> tactic -> tactic"} \\
+  @{index_ML CHANGED: "tactic -> tactic"} \\
+  \end{mldecls}
+
+  \begin{description}
+
+  \item @{ML FILTER}~@{text "sat tac"} applies @{text "tac"} to the
+  goal state and returns a sequence consisting of those result goal
+  states that are satisfactory in the sense of @{text "sat"}.
+
+  \item @{ML CHANGED}~@{text "tac"} applies @{text "tac"} to the goal
+  state and returns precisely those states that differ from the
+  original state (according to @{ML Thm.eq_thm}).  Thus @{ML
+  CHANGED}~@{text "tac"} always has some effect on the state.
+
+  \end{description}
+*}
+
+
+subsubsection {* Depth-first search *}
+
+text {*
+  \begin{mldecls}
+  @{index_ML DEPTH_FIRST: "(thm -> bool) -> tactic -> tactic"} \\
+  @{index_ML DEPTH_SOLVE: "tactic -> tactic"} \\
+  @{index_ML DEPTH_SOLVE_1: "tactic -> tactic"} \\
+  \end{mldecls}
+
+  \begin{description}
+
+  \item @{ML DEPTH_FIRST}~@{text "sat tac"} returns the goal state if
+  @{text "sat"} returns true.  Otherwise it applies @{text "tac"},
+  then recursively searches from each element of the resulting
+  sequence.  The code uses a stack for efficiency, in effect applying
+  @{text "tac"}~@{ML_op THEN}~@{ML DEPTH_FIRST}~@{text "sat tac"} to
+  the state.
+
+  \item @{ML DEPTH_SOLVE}@{text "tac"} uses @{ML DEPTH_FIRST} to
+  search for states having no subgoals.
+
+  \item @{ML DEPTH_SOLVE_1}~@{text "tac"} uses @{ML DEPTH_FIRST} to
+  search for states having fewer subgoals than the given state.  Thus,
+  it insists upon solving at least one subgoal.
+
+  \end{description}
+*}
+
+
+subsubsection {* Other search strategies *}
+
+text {*
+  \begin{mldecls}
+  @{index_ML BREADTH_FIRST: "(thm -> bool) -> tactic -> tactic"} \\
+  @{index_ML BEST_FIRST: "(thm -> bool) * (thm -> int) -> tactic -> tactic"} \\
+  @{index_ML THEN_BEST_FIRST: "tactic -> (thm -> bool) * (thm -> int) -> tactic -> tactic"} \\
+  \end{mldecls}
+
+  These search strategies will find a solution if one exists.
+  However, they do not enumerate all solutions; they terminate after
+  the first satisfactory result from @{text "tac"}.
+
+  \begin{description}
+
+  \item @{ML BREADTH_FIRST}~@{text "sat tac"} uses breadth-first
+  search to find states for which @{text "sat"} is true.  For most
+  applications, it is too slow.
+
+  \item @{ML BEST_FIRST}~@{text "(sat, dist) tac"} does a heuristic
+  search, using @{text "dist"} to estimate the distance from a
+  satisfactory state (in the sense of @{text "sat"}).  It maintains a
+  list of states ordered by distance.  It applies @{text "tac"} to the
+  head of this list; if the result contains any satisfactory states,
+  then it returns them.  Otherwise, @{ML BEST_FIRST} adds the new
+  states to the list, and continues.
+
+  The distance function is typically @{ML size_of_thm}, which computes
+  the size of the state.  The smaller the state, the fewer and simpler
+  subgoals it has.
+
+  \item @{ML THEN_BEST_FIRST}~@{text "tac\<^sub>0 (sat, dist) tac"} is like
+  @{ML BEST_FIRST}, except that the priority queue initially contains
+  the result of applying @{text "tac\<^sub>0"} to the goal state.  This
+  tactical permits separate tactics for starting the search and
+  continuing the search.
+
+  \end{description}
+*}
+
+
+subsubsection {* Auxiliary tacticals for searching *}
+
+text {*
+  \begin{mldecls}
+  @{index_ML COND: "(thm -> bool) -> tactic -> tactic -> tactic"} \\
+  @{index_ML IF_UNSOLVED: "tactic -> tactic"} \\
+  @{index_ML SOLVE: "tactic -> tactic"} \\
+  @{index_ML DETERM: "tactic -> tactic"} \\
+  \end{mldecls}
+
+  \begin{description}
+
+  \item @{ML COND}~@{text "sat tac\<^sub>1 tac\<^sub>2"} applies @{text "tac\<^sub>1"} to
+  the goal state if it satisfies predicate @{text "sat"}, and applies
+  @{text "tac\<^sub>2"}.  It is a conditional tactical in that only one of
+  @{text "tac\<^sub>1"} and @{text "tac\<^sub>2"} is applied to a goal state.
+  However, both @{text "tac\<^sub>1"} and @{text "tac\<^sub>2"} are evaluated
+  because ML uses eager evaluation.
+
+  \item @{ML IF_UNSOLVED}~@{text "tac"} applies @{text "tac"} to the
+  goal state if it has any subgoals, and simply returns the goal state
+  otherwise.  Many common tactics, such as @{ML resolve_tac}, fail if
+  applied to a goal state that has no subgoals.
+
+  \item @{ML SOLVE}~@{text "tac"} applies @{text "tac"} to the goal
+  state and then fails iff there are subgoals left.
+
+  \item @{ML DETERM}~@{text "tac"} applies @{text "tac"} to the goal
+  state and returns the head of the resulting sequence.  @{ML DETERM}
+  limits the search space by making its argument deterministic.
+
+  \end{description}
+*}
+
+
+subsubsection {* Predicates and functions useful for searching *}
+
+text {*
+  \begin{mldecls}
+  @{index_ML has_fewer_prems: "int -> thm -> bool"} \\
+  @{index_ML Thm.eq_thm: "thm * thm -> bool"} \\
+  @{index_ML Thm.eq_thm_prop: "thm * thm -> bool"} \\
+  @{index_ML size_of_thm: "thm -> int"} \\
+  \end{mldecls}
+
+  \begin{description}
+
+  \item @{ML has_fewer_prems}~@{text "n thm"} reports whether @{text
+  "thm"} has fewer than @{text "n"} premises.
+
+  \item @{ML Thm.eq_thm}~@{text "(thm\<^sub>1, thm\<^sub>2)"} reports whether @{text
+  "thm\<^sub>1"} and @{text "thm\<^sub>2"} are equal.  Both theorems must have
+  compatible background theories.  Both theorems must have the same
+  conclusions, the same set of hypotheses, and the same set of sort
+  hypotheses.  Names of bound variables are ignored as usual.
+
+  \item @{ML Thm.eq_thm_prop}~@{text "(thm\<^sub>1, thm\<^sub>2)"} reports whether
+  the propositions of @{text "thm\<^sub>1"} and @{text "thm\<^sub>2"} are equal.
+  Names of bound variables are ignored.
+
+  \item @{ML size_of_thm}~@{text "thm"} computes the size of @{text
+  "thm"}, namely the number of variables, constants and abstractions
+  in its conclusion.  It may serve as a distance function for
+  @{ML BEST_FIRST}.
+
+  \end{description}
+*}
+
 end

--- a/doc-src/IsarImplementation/Thy/document/Tactic.tex	Thu Jan 26 21:25:18 2012 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Tactic.tex	Thu Jan 26 22:16:45 2012 +0100
@@ -480,10 +480,7 @@
   complex tactics from simpler ones.  Common tacticals perform
   sequential composition, disjunctive choice, iteration, or goal
   addressing.  Various search strategies may be expressed via
-  tacticals.
-
-  \medskip The chapter on tacticals in old \cite{isabelle-ref} is
-  still applicable for further details.%
+  tacticals.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -525,13 +522,12 @@
   \begin{description}
 
   \item \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}}~\verb|THEN|~\isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} is the sequential
-  composition of \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} and \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}}.  Applied to a
-  proof state, it returns all states reachable in two steps by
-  applying \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} followed by \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}}.  First, it
-  applies \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} to the proof state, getting a sequence of
-  possible next states; then, it applies \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} to each of
-  these and concatenates the results to produce again one flat
-  sequence of states.
+  composition of \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} and \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}}.  Applied to a goal
+  state, it returns all states reachable in two steps by applying
+  \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} followed by \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}}.  First, it applies \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} to the goal state, getting a sequence of possible next
+  states; then, it applies \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} to each of these and
+  concatenates the results to produce again one flat sequence of
+  states.
 
   \item \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}}~\verb|ORELSE|~\isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} makes a choice
   between \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} and \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}}.  Applied to a state, it
@@ -596,7 +592,7 @@
 
   \begin{description}
 
-  \item \verb|TRY|~\isa{tac} applies \isa{tac} to the proof
+  \item \verb|TRY|~\isa{tac} applies \isa{tac} to the goal
   state and returns the resulting sequence, if non-empty; otherwise it
   returns the original state.  Thus, it applies \isa{tac} at most
   once.
@@ -604,7 +600,7 @@
   Note that for tactics with subgoal addressing, the combinator can be
   applied via functional composition: \verb|TRY|~\verb|o|~\isa{tac}.  There is no need for \verb|TRY'|.
 
-  \item \verb|REPEAT|~\isa{tac} applies \isa{tac} to the proof
+  \item \verb|REPEAT|~\isa{tac} applies \isa{tac} to the goal
   state and, recursively, to each element of the resulting sequence.
   The resulting sequence consists of those states that make \isa{tac} fail.  Thus, it applies \isa{tac} as many times as
   possible (including zero times), and allows backtracking over each
@@ -615,7 +611,7 @@
   is impossible.
 
   \item \verb|REPEAT_DETERM|~\isa{tac} applies \isa{tac} to the
-  proof state and, recursively, to the head of the resulting sequence.
+  goal state and, recursively, to the head of the resulting sequence.
   It returns the first state to make \isa{tac} fail.  It is
   deterministic, discarding alternative outcomes.
 
@@ -690,7 +686,7 @@
   possible in each outcome.
 
   \begin{warn}
-  Note the explicit abstraction over the proof state in the ML
+  Note the explicit abstraction over the goal state in the ML
   definition of \verb|REPEAT|.  Recursive tacticals must be coded in
   this awkward fashion to avoid infinite recursion of eager functional
   evaluation in Standard ML.  The following attempt would make \verb|REPEAT|~\isa{tac} loop:
@@ -787,6 +783,189 @@
 %
 \endisadelimmlref
 %
+\isamarkupsubsection{Control and search tacticals%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+A predicate on theorems \verb|thm -> bool| can test
+  whether a goal state enjoys some desirable property --- such as
+  having no subgoals.  Tactics that search for satisfactory goal
+  states are easy to express.  The main search procedures,
+  depth-first, breadth-first and best-first, are provided as
+  tacticals.  They generate the search tree by repeatedly applying a
+  given tactic.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{Filtering a tactic's results%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{mldecls}
+  \indexdef{}{ML}{FILTER}\verb|FILTER: (thm -> bool) -> tactic -> tactic| \\
+  \indexdef{}{ML}{CHANGED}\verb|CHANGED: tactic -> tactic| \\
+  \end{mldecls}
+
+  \begin{description}
+
+  \item \verb|FILTER|~\isa{sat\ tac} applies \isa{tac} to the
+  goal state and returns a sequence consisting of those result goal
+  states that are satisfactory in the sense of \isa{sat}.
+
+  \item \verb|CHANGED|~\isa{tac} applies \isa{tac} to the goal
+  state and returns precisely those states that differ from the
+  original state (according to \verb|Thm.eq_thm|).  Thus \verb|CHANGED|~\isa{tac} always has some effect on the state.
+
+  \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{Depth-first search%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{mldecls}
+  \indexdef{}{ML}{DEPTH\_FIRST}\verb|DEPTH_FIRST: (thm -> bool) -> tactic -> tactic| \\
+  \indexdef{}{ML}{DEPTH\_SOLVE}\verb|DEPTH_SOLVE: tactic -> tactic| \\
+  \indexdef{}{ML}{DEPTH\_SOLVE\_1}\verb|DEPTH_SOLVE_1: tactic -> tactic| \\
+  \end{mldecls}
+
+  \begin{description}
+
+  \item \verb|DEPTH_FIRST|~\isa{sat\ tac} returns the goal state if
+  \isa{sat} returns true.  Otherwise it applies \isa{tac},
+  then recursively searches from each element of the resulting
+  sequence.  The code uses a stack for efficiency, in effect applying
+  \isa{tac}~\verb|THEN|~\verb|DEPTH_FIRST|~\isa{sat\ tac} to
+  the state.
+
+  \item \verb|DEPTH_SOLVE|\isa{tac} uses \verb|DEPTH_FIRST| to
+  search for states having no subgoals.
+
+  \item \verb|DEPTH_SOLVE_1|~\isa{tac} uses \verb|DEPTH_FIRST| to
+  search for states having fewer subgoals than the given state.  Thus,
+  it insists upon solving at least one subgoal.
+
+  \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{Other search strategies%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{mldecls}
+  \indexdef{}{ML}{BREADTH\_FIRST}\verb|BREADTH_FIRST: (thm -> bool) -> tactic -> tactic| \\
+  \indexdef{}{ML}{BEST\_FIRST}\verb|BEST_FIRST: (thm -> bool) * (thm -> int) -> tactic -> tactic| \\
+  \indexdef{}{ML}{THEN\_BEST\_FIRST}\verb|THEN_BEST_FIRST: tactic -> (thm -> bool) * (thm -> int) -> tactic -> tactic| \\
+  \end{mldecls}
+
+  These search strategies will find a solution if one exists.
+  However, they do not enumerate all solutions; they terminate after
+  the first satisfactory result from \isa{tac}.
+
+  \begin{description}
+
+  \item \verb|BREADTH_FIRST|~\isa{sat\ tac} uses breadth-first
+  search to find states for which \isa{sat} is true.  For most
+  applications, it is too slow.
+
+  \item \verb|BEST_FIRST|~\isa{{\isaliteral{28}{\isacharparenleft}}sat{\isaliteral{2C}{\isacharcomma}}\ dist{\isaliteral{29}{\isacharparenright}}\ tac} does a heuristic
+  search, using \isa{dist} to estimate the distance from a
+  satisfactory state (in the sense of \isa{sat}).  It maintains a
+  list of states ordered by distance.  It applies \isa{tac} to the
+  head of this list; if the result contains any satisfactory states,
+  then it returns them.  Otherwise, \verb|BEST_FIRST| adds the new
+  states to the list, and continues.
+
+  The distance function is typically \verb|size_of_thm|, which computes
+  the size of the state.  The smaller the state, the fewer and simpler
+  subgoals it has.
+
+  \item \verb|THEN_BEST_FIRST|~\isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{0}}\ {\isaliteral{28}{\isacharparenleft}}sat{\isaliteral{2C}{\isacharcomma}}\ dist{\isaliteral{29}{\isacharparenright}}\ tac} is like
+  \verb|BEST_FIRST|, except that the priority queue initially contains
+  the result of applying \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{0}}} to the goal state.  This
+  tactical permits separate tactics for starting the search and
+  continuing the search.
+
+  \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{Auxiliary tacticals for searching%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{mldecls}
+  \indexdef{}{ML}{COND}\verb|COND: (thm -> bool) -> tactic -> tactic -> tactic| \\
+  \indexdef{}{ML}{IF\_UNSOLVED}\verb|IF_UNSOLVED: tactic -> tactic| \\
+  \indexdef{}{ML}{SOLVE}\verb|SOLVE: tactic -> tactic| \\
+  \indexdef{}{ML}{DETERM}\verb|DETERM: tactic -> tactic| \\
+  \end{mldecls}
+
+  \begin{description}
+
+  \item \verb|COND|~\isa{sat\ tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} applies \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} to
+  the goal state if it satisfies predicate \isa{sat}, and applies
+  \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}}.  It is a conditional tactical in that only one of
+  \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} and \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} is applied to a goal state.
+  However, both \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} and \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} are evaluated
+  because ML uses eager evaluation.
+
+  \item \verb|IF_UNSOLVED|~\isa{tac} applies \isa{tac} to the
+  goal state if it has any subgoals, and simply returns the goal state
+  otherwise.  Many common tactics, such as \verb|resolve_tac|, fail if
+  applied to a goal state that has no subgoals.
+
+  \item \verb|SOLVE|~\isa{tac} applies \isa{tac} to the goal
+  state and then fails iff there are subgoals left.
+
+  \item \verb|DETERM|~\isa{tac} applies \isa{tac} to the goal
+  state and returns the head of the resulting sequence.  \verb|DETERM|
+  limits the search space by making its argument deterministic.
+
+  \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{Predicates and functions useful for searching%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{mldecls}
+  \indexdef{}{ML}{has\_fewer\_prems}\verb|has_fewer_prems: int -> thm -> bool| \\
+  \indexdef{}{ML}{Thm.eq\_thm}\verb|Thm.eq_thm: thm * thm -> bool| \\
+  \indexdef{}{ML}{Thm.eq\_thm\_prop}\verb|Thm.eq_thm_prop: thm * thm -> bool| \\
+  \indexdef{}{ML}{size\_of\_thm}\verb|size_of_thm: thm -> int| \\
+  \end{mldecls}
+
+  \begin{description}
+
+  \item \verb|has_fewer_prems|~\isa{n\ thm} reports whether \isa{thm} has fewer than \isa{n} premises.
+
+  \item \verb|Thm.eq_thm|~\isa{{\isaliteral{28}{\isacharparenleft}}thm\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ thm\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}} reports whether \isa{thm\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} and \isa{thm\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} are equal.  Both theorems must have
+  compatible background theories.  Both theorems must have the same
+  conclusions, the same set of hypotheses, and the same set of sort
+  hypotheses.  Names of bound variables are ignored as usual.
+
+  \item \verb|Thm.eq_thm_prop|~\isa{{\isaliteral{28}{\isacharparenleft}}thm\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ thm\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}} reports whether
+  the propositions of \isa{thm\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} and \isa{thm\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} are equal.
+  Names of bound variables are ignored.
+
+  \item \verb|size_of_thm|~\isa{thm} computes the size of \isa{thm}, namely the number of variables, constants and abstractions
+  in its conclusion.  It may serve as a distance function for
+  \verb|BEST_FIRST|.
+
+  \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
 \isadelimtheory
 %
 \endisadelimtheory

--- a/doc-src/Ref/Makefile	Thu Jan 26 21:25:18 2012 +0100
+++ b/doc-src/Ref/Makefile	Thu Jan 26 22:16:45 2012 +0100
@@ -9,7 +9,7 @@
 include ../Makefile.in
 
 NAME = ref
-FILES = ref.tex tactic.tex tctical.tex thm.tex defining.tex syntax.tex	\
+FILES = ref.tex tactic.tex thm.tex defining.tex syntax.tex		\
 	substitution.tex simplifier.tex classical.tex ../proof.sty	\
 	../iman.sty ../extra.sty ../ttbox.sty ../manual.bib
 

--- a/doc-src/Ref/ref.tex	Thu Jan 26 21:25:18 2012 +0100
+++ b/doc-src/Ref/ref.tex	Thu Jan 26 22:16:45 2012 +0100
@@ -48,7 +48,6 @@
 \pagenumbering{roman} \tableofcontents \clearfirst
 
 \include{tactic}
-\include{tctical}
 \include{thm}
 \include{defining}
 \include{syntax}

--- a/doc-src/Ref/tctical.tex	Thu Jan 26 21:25:18 2012 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,176 +0,0 @@
-
-\chapter{Tacticals}
-
-\section{Control and search tacticals}
-\index{search!tacticals|(}
-
-A predicate on theorems, namely a function of type \hbox{\tt thm->bool},
-can test whether a proof state enjoys some desirable property --- such as
-having no subgoals.  Tactics that search for satisfactory states are easy
-to express.  The main search procedures, depth-first, breadth-first and
-best-first, are provided as tacticals.  They generate the search tree by
-repeatedly applying a given tactic.
-
-
-\subsection{Filtering a tactic's results}
-\index{tacticals!for filtering}
-\index{tactics!filtering results of}
-\begin{ttbox} 
-FILTER  : (thm -> bool) -> tactic -> tactic
-CHANGED : tactic -> tactic
-\end{ttbox}
-\begin{ttdescription}
-\item[\ttindexbold{FILTER} {\it p} $tac$] 
-applies $tac$ to the proof state and returns a sequence consisting of those
-result states that satisfy~$p$.
-
-\item[\ttindexbold{CHANGED} {\it tac}] 
-applies {\it tac\/} to the proof state and returns precisely those states
-that differ from the original state.  Thus, \hbox{\tt CHANGED {\it tac}}
-always has some effect on the state.
-\end{ttdescription}
-
-
-\subsection{Depth-first search}
-\index{tacticals!searching}
-\index{tracing!of searching tacticals}
-\begin{ttbox} 
-DEPTH_FIRST   : (thm->bool) -> tactic -> tactic
-DEPTH_SOLVE   :                tactic -> tactic
-DEPTH_SOLVE_1 :                tactic -> tactic
-trace_DEPTH_FIRST: bool ref \hfill{\bf initially false}
-\end{ttbox}
-\begin{ttdescription}
-\item[\ttindexbold{DEPTH_FIRST} {\it satp} {\it tac}] 
-returns the proof state if {\it satp} returns true.  Otherwise it applies
-{\it tac}, then recursively searches from each element of the resulting
-sequence.  The code uses a stack for efficiency, in effect applying
-\hbox{\tt {\it tac} THEN DEPTH_FIRST {\it satp} {\it tac}} to the state.
-
-\item[\ttindexbold{DEPTH_SOLVE} {\it tac}] 
-uses {\tt DEPTH_FIRST} to search for states having no subgoals.
-
-\item[\ttindexbold{DEPTH_SOLVE_1} {\it tac}] 
-uses {\tt DEPTH_FIRST} to search for states having fewer subgoals than the
-given state.  Thus, it insists upon solving at least one subgoal.
-
-\item[set \ttindexbold{trace_DEPTH_FIRST};] 
-enables interactive tracing for {\tt DEPTH_FIRST}.  To view the
-tracing options, type {\tt h} at the prompt.
-\end{ttdescription}
-
-
-\subsection{Other search strategies}
-\index{tacticals!searching}
-\index{tracing!of searching tacticals}
-\begin{ttbox} 
-BREADTH_FIRST   :            (thm->bool) -> tactic -> tactic
-BEST_FIRST      : (thm->bool)*(thm->int) -> tactic -> tactic
-THEN_BEST_FIRST : tactic * ((thm->bool) * (thm->int) * tactic)
-                  -> tactic                    \hfill{\bf infix 1}
-trace_BEST_FIRST: bool ref \hfill{\bf initially false}
-\end{ttbox}
-These search strategies will find a solution if one exists.  However, they
-do not enumerate all solutions; they terminate after the first satisfactory
-result from {\it tac}.
-\begin{ttdescription}
-\item[\ttindexbold{BREADTH_FIRST} {\it satp} {\it tac}] 
-uses breadth-first search to find states for which {\it satp\/} is true.
-For most applications, it is too slow.
-
-\item[\ttindexbold{BEST_FIRST} $(satp,distf)$ {\it tac}] 
-does a heuristic search, using {\it distf\/} to estimate the distance from
-a satisfactory state.  It maintains a list of states ordered by distance.
-It applies $tac$ to the head of this list; if the result contains any
-satisfactory states, then it returns them.  Otherwise, {\tt BEST_FIRST}
-adds the new states to the list, and continues.  
-
-The distance function is typically \ttindex{size_of_thm}, which computes
-the size of the state.  The smaller the state, the fewer and simpler
-subgoals it has.
-
-\item[$tac@0$ \ttindexbold{THEN_BEST_FIRST} $(satp,distf,tac)$] 
-is like {\tt BEST_FIRST}, except that the priority queue initially
-contains the result of applying $tac@0$ to the proof state.  This tactical
-permits separate tactics for starting the search and continuing the search.
-
-\item[set \ttindexbold{trace_BEST_FIRST};] 
-enables an interactive tracing mode for the tactical {\tt BEST_FIRST}.  To
-view the tracing options, type {\tt h} at the prompt.
-\end{ttdescription}
-
-
-\subsection{Auxiliary tacticals for searching}
-\index{tacticals!conditional}
-\index{tacticals!deterministic}
-\begin{ttbox} 
-COND                : (thm->bool) -> tactic -> tactic -> tactic
-IF_UNSOLVED         : tactic -> tactic
-SOLVE               : tactic -> tactic
-DETERM              : tactic -> tactic
-DETERM_UNTIL_SOLVED : tactic -> tactic
-\end{ttbox}
-\begin{ttdescription}
-\item[\ttindexbold{COND} {\it p} $tac@1$ $tac@2$] 
-applies $tac@1$ to the proof state if it satisfies~$p$, and applies $tac@2$
-otherwise.  It is a conditional tactical in that only one of $tac@1$ and
-$tac@2$ is applied to a proof state.  However, both $tac@1$ and $tac@2$ are
-evaluated because \ML{} uses eager evaluation.
-
-\item[\ttindexbold{IF_UNSOLVED} {\it tac}] 
-applies {\it tac\/} to the proof state if it has any subgoals, and simply
-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
-argument deterministic.
-
-\item[\ttindexbold{DETERM_UNTIL_SOLVED} {\it tac}] 
-forces repeated deterministic application of {\it tac\/} to the proof state 
-until the goal is solved completely.
-\end{ttdescription}
-
-
-\subsection{Predicates and functions useful for searching}
-\index{theorems!size of}
-\index{theorems!equality of}
-\begin{ttbox} 
-has_fewer_prems : int -> thm -> bool
-eq_thm          : thm * thm -> bool
-eq_thm_prop     : thm * thm -> bool
-size_of_thm     : thm -> int
-\end{ttbox}
-\begin{ttdescription}
-\item[\ttindexbold{has_fewer_prems} $n$ $thm$] 
-reports whether $thm$ has fewer than~$n$ premises.  By currying,
-\hbox{\tt has_fewer_prems $n$} is a predicate on theorems; it may 
-be given to the searching tacticals.
-
-\item[\ttindexbold{eq_thm} ($thm@1$, $thm@2$)] reports whether $thm@1$ and
-  $thm@2$ are equal.  Both theorems must have compatible signatures.  Both
-  theorems must have the same conclusions, the same hypotheses (in the same
-  order), and the same set of sort hypotheses.  Names of bound variables are
-  ignored.
-  
-\item[\ttindexbold{eq_thm_prop} ($thm@1$, $thm@2$)] reports whether the
-  propositions of $thm@1$ and $thm@2$ are equal.  Names of bound variables are
-  ignored.
-
-\item[\ttindexbold{size_of_thm} $thm$] 
-computes the size of $thm$, namely the number of variables, constants and
-abstractions in its conclusion.  It may serve as a distance function for 
-\ttindex{BEST_FIRST}. 
-\end{ttdescription}
-
-\index{search!tacticals|)}
-
-%%% Local Variables: 
-%%% mode: latex
-%%% TeX-master: "ref"
-%%% End: