1.1 --- a/doc-src/Ref/tactic.tex	Wed Jan 25 15:39:08 2012 +0100
     1.2 +++ b/doc-src/Ref/tactic.tex	Wed Jan 25 16:16:20 2012 +0100
     1.3 @@ -38,22 +38,6 @@
     1.4  \end{ttdescription}
     1.5  
     1.6  
     1.7 -\subsection{``Putting off'' a subgoal}
     1.8 -\begin{ttbox} 
     1.9 -defer_tac : int -> tactic
    1.10 -\end{ttbox}
    1.11 -\begin{ttdescription}
    1.12 -\item[\ttindexbold{defer_tac} {\it i}] 
    1.13 -  moves subgoal~$i$ to the last position in the proof state.  It can be
    1.14 -  useful when correcting a proof script: if the tactic given for subgoal~$i$
    1.15 -  fails, calling {\tt defer_tac} instead will let you continue with the rest
    1.16 -  of the script.
    1.17 -
    1.18 -  The tactic fails if subgoal~$i$ does not exist or if the proof state
    1.19 -  contains type unknowns. 
    1.20 -\end{ttdescription}
    1.21 -
    1.22 -
    1.23  \subsection{Definitions and meta-level rewriting} \label{sec:rewrite_goals}
    1.24  \index{tactics!meta-rewriting|bold}\index{meta-rewriting|bold}
    1.25  \index{definitions}
    1.26 @@ -68,13 +52,10 @@
    1.27  
    1.28  There are rules for unfolding and folding definitions; Isabelle does not do
    1.29  this automatically.  The corresponding tactics rewrite the proof state,
    1.30 -yielding a single next state.  See also the {\tt goalw} command, which is the
    1.31 -easiest way of handling definitions.
    1.32 +yielding a single next state.
    1.33  \begin{ttbox} 
    1.34  rewrite_goals_tac : thm list -> tactic
    1.35 -rewrite_tac       : thm list -> tactic
    1.36  fold_goals_tac    : thm list -> tactic
    1.37 -fold_tac          : thm list -> tactic
    1.38  \end{ttbox}
    1.39  \begin{ttdescription}
    1.40  \item[\ttindexbold{rewrite_goals_tac} {\it defs}]  
    1.41 @@ -82,16 +63,9 @@
    1.42  leaving the main goal unchanged.  Use \ttindex{SELECT_GOAL} to restrict it to a
    1.43  particular subgoal.
    1.44  
    1.45 -\item[\ttindexbold{rewrite_tac} {\it defs}]  
    1.46 -unfolds the {\it defs} throughout the proof state, including the main goal
    1.47 ---- not normally desirable!
    1.48 -
    1.49  \item[\ttindexbold{fold_goals_tac} {\it defs}]  
    1.50  folds the {\it defs} throughout the subgoals of the proof state, while
    1.51  leaving the main goal unchanged.
    1.52 -
    1.53 -\item[\ttindexbold{fold_tac} {\it defs}]  
    1.54 -folds the {\it defs} throughout the proof state.
    1.55  \end{ttdescription}
    1.56  
    1.57  \begin{warn}

     2.1 --- a/doc-src/Ref/tctical.tex	Wed Jan 25 15:39:08 2012 +0100
     2.2 +++ b/doc-src/Ref/tctical.tex	Wed Jan 25 16:16:20 2012 +0100
     2.3 @@ -344,16 +344,15 @@
     2.4  \index{tacticals!for restriction to a subgoal}
     2.5  \begin{ttbox} 
     2.6  SELECT_GOAL : tactic -> int -> tactic
     2.7 -METAHYPS    : (thm list -> tactic) -> int -> tactic
     2.8  \end{ttbox}
     2.9  \begin{ttdescription}
    2.10  \item[\ttindexbold{SELECT_GOAL} {\it tac} $i$] 
    2.11  restricts the effect of {\it tac\/} to subgoal~$i$ of the proof state.  It
    2.12 -fails if there is no subgoal~$i$, or if {\it tac\/} changes the main goal
    2.13 -(do not use {\tt rewrite_tac}).  It applies {\it tac\/} to a dummy proof
    2.14 -state and uses the result to refine the original proof state at
    2.15 -subgoal~$i$.  If {\it tac\/} returns multiple results then so does 
    2.16 -\hbox{\tt SELECT_GOAL {\it tac} $i$}.
    2.17 +fails if there is no subgoal~$i$, or if {\it tac\/} changes the main goal.
    2.18 +It applies {\it tac\/} to a dummy proof state and uses the result to
    2.19 +refine the original proof state at subgoal~$i$.  If {\it tac\/}
    2.20 +returns multiple results then so does \hbox{\tt SELECT_GOAL {\it tac}
    2.21 +  $i$}.
    2.22  
    2.23  {\tt SELECT_GOAL} works by creating a state of the form $\phi\Imp\phi$,
    2.24  with the one subgoal~$\phi$.  If subgoal~$i$ has the form $\psi\Imp\theta$
    2.25 @@ -363,40 +362,8 @@
    2.26    SELECT_GOAL} inserts a quantifier to create the state
    2.27  \[ (\Forall x.\psi\Imp\theta)\Imp(\Forall x.\psi\Imp\theta). \]
    2.28  
    2.29 -\item[\ttindexbold{METAHYPS} {\it tacf} $i$]\index{meta-assumptions}
    2.30 -takes subgoal~$i$, of the form 
    2.31 -\[ \Forall x@1 \ldots x@l. \List{\theta@1; \ldots; \theta@k}\Imp\theta, \]
    2.32 -and creates the list $\theta'@1$, \ldots, $\theta'@k$ of meta-level
    2.33 -assumptions.  In these theorems, the subgoal's parameters ($x@1$,
    2.34 -\ldots,~$x@l$) become free variables.  It supplies the assumptions to
    2.35 -$tacf$ and applies the resulting tactic to the proof state
    2.36 -$\theta\Imp\theta$.
    2.37 -
    2.38 -If the resulting proof state is $\List{\phi@1; \ldots; \phi@n} \Imp \phi$,
    2.39 -possibly containing $\theta'@1,\ldots,\theta'@k$ as assumptions, then it is
    2.40 -lifted back into the original context, yielding $n$ subgoals.
    2.41 -
    2.42 -Meta-level assumptions may not contain unknowns.  Unknowns in the
    2.43 -hypotheses $\theta@1,\ldots,\theta@k$ become free variables in $\theta'@1$,
    2.44 -\ldots, $\theta'@k$, and are restored afterwards; the {\tt METAHYPS} call
    2.45 -cannot instantiate them.  Unknowns in $\theta$ may be instantiated.  New
    2.46 -unknowns in $\phi@1$, \ldots, $\phi@n$ are lifted over the parameters.
    2.47 -
    2.48 -Here is a typical application.  Calling {\tt hyp_res_tac}~$i$ resolves
    2.49 -subgoal~$i$ with one of its own assumptions, which may itself have the form
    2.50 -of an inference rule (these are called {\bf higher-level assumptions}).  
    2.51 -\begin{ttbox} 
    2.52 -val hyp_res_tac = METAHYPS (fn prems => resolve_tac prems 1);
    2.53 -\end{ttbox} 
    2.54 -The function \ttindex{gethyps} is useful for debugging applications of {\tt
    2.55 -  METAHYPS}. 
    2.56  \end{ttdescription}
    2.57  
    2.58 -\begin{warn}
    2.59 -{\tt METAHYPS} fails if the context or new subgoals contain type unknowns.
    2.60 -In principle, the tactical could treat these like ordinary unknowns.
    2.61 -\end{warn}
    2.62 -
    2.63  
    2.64  \subsection{Scanning for a subgoal by number}
    2.65  \index{tacticals!scanning for subgoals}

     3.1 --- a/doc-src/Ref/thm.tex	Wed Jan 25 15:39:08 2012 +0100
     3.2 +++ b/doc-src/Ref/thm.tex	Wed Jan 25 16:16:20 2012 +0100
     3.3 @@ -143,7 +143,6 @@
     3.4  nprems_of     : thm -> int
     3.5  tpairs_of     : thm -> (term*term) list
     3.6  theory_of_thm : thm -> theory
     3.7 -dest_state : thm * int -> (term*term) list * term list * term * term
     3.8  \end{ttbox}
     3.9  \begin{ttdescription}
    3.10  \item[\ttindexbold{cprop_of} $thm$] returns the statement of $thm$ as
    3.11 @@ -169,11 +168,6 @@
    3.12    with $thm$.  Note that this does a lookup in Isabelle's global
    3.13    database of loaded theories.
    3.14  
    3.15 -\item[\ttindexbold{dest_state} $(thm,i)$] 
    3.16 -decomposes $thm$ as a tuple containing a list of flex-flex constraints, a
    3.17 -list of the subgoals~1 to~$i-1$, subgoal~$i$, and the rest of the theorem
    3.18 -(this will be an implication if there are more than $i$ subgoals).
    3.19 -
    3.20  \end{ttdescription}
    3.21  
    3.22