author wenzelm Thu, 26 Jan 2012 21:25:18 +0100 changeset 46268 45ce067a7562 parent 46267 bc9479cada96 child 46269 e75181672150
obsolete -- covered in implementation manual;
 doc-src/Ref/tctical.tex file | annotate | diff | comparison | revisions
--- a/doc-src/Ref/tctical.tex	Thu Jan 26 21:16:11 2012 +0100
+++ b/doc-src/Ref/tctical.tex	Thu Jan 26 21:25:18 2012 +0100
@@ -170,43 +170,6 @@

\index{search!tacticals|)}

-
-\section{Tacticals for subgoal numbering}
-When conducting a backward proof, we normally consider one goal at a time.
-A tactic can affect the entire proof state, but many tactics --- such as
-{\tt resolve_tac} and {\tt assume_tac} --- work on a single subgoal.
-Subgoals are designated by a positive integer, so Isabelle provides
-tacticals for combining values of type {\tt int->tactic}.
-
-
-\subsection{Restricting a tactic to one subgoal}
-\index{tactics!restricting to a subgoal}
-\index{tacticals!for restriction to a subgoal}
-\begin{ttbox}
-SELECT_GOAL : tactic -> int -> tactic
-\end{ttbox}
-\begin{ttdescription}
-\item[\ttindexbold{SELECT_GOAL} {\it tac} $i$]
-restricts the effect of {\it tac\/} to subgoal~$i$ of the proof state.  It
-fails if there is no subgoal~$i$, or if {\it tac\/} changes the main goal.
-It applies {\it tac\/} to a dummy proof state and uses the result to
-refine the original proof state at subgoal~$i$.  If {\it tac\/}
-returns multiple results then so does \hbox{\tt SELECT_GOAL {\it tac}
-  $i$}.
-
-{\tt SELECT_GOAL} works by creating a state of the form $\phi\Imp\phi$,
-with the one subgoal~$\phi$.  If subgoal~$i$ has the form $\psi\Imp\theta$
-then $(\psi\Imp\theta)\Imp(\psi\Imp\theta)$ is in fact
-$\List{\psi\Imp\theta;\; \psi}\Imp\theta$, a proof state with two subgoals.
-Such a proof state might cause tactics to go astray.  Therefore {\tt
-  SELECT_GOAL} inserts a quantifier to create the state
-$(\Forall x.\psi\Imp\theta)\Imp(\Forall x.\psi\Imp\theta).$
-
-\end{ttdescription}
-
-\index{tacticals|)}
-
-
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "ref"