# HG changeset patch # User wenzelm # Date 1327609518 -3600 # Node ID 45ce067a75627aecbf7c3f8ca2dbb9eded60690f # Parent bc9479cada965ba7dfbc365120e7e11270355779 obsolete -- covered in implementation manual; diff -r bc9479cada96 -r 45ce067a7562 doc-src/Ref/tctical.tex --- 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"