# HG changeset patch
# User wenzelm
# Date 1327504580 -3600
# Node ID 3ba3681d89301cda16dd1022b7e73a043caf2036
# Parent  bc874d2ee55a5b7e6e84b53728bb63c160995246
removed obscure/outdated material;

diff -r bc874d2ee55a -r 3ba3681d8930 doc-src/Ref/tactic.tex
--- a/doc-src/Ref/tactic.tex	Wed Jan 25 15:39:08 2012 +0100
+++ b/doc-src/Ref/tactic.tex	Wed Jan 25 16:16:20 2012 +0100
@@ -38,22 +38,6 @@
 \end{ttdescription}
 
 
-\subsection{``Putting off'' a subgoal}
-\begin{ttbox} 
-defer_tac : int -> tactic
-\end{ttbox}
-\begin{ttdescription}
-\item[\ttindexbold{defer_tac} {\it i}] 
-  moves subgoal~$i$ to the last position in the proof state.  It can be
-  useful when correcting a proof script: if the tactic given for subgoal~$i$
-  fails, calling {\tt defer_tac} instead will let you continue with the rest
-  of the script.
-
-  The tactic fails if subgoal~$i$ does not exist or if the proof state
-  contains type unknowns. 
-\end{ttdescription}
-
-
 \subsection{Definitions and meta-level rewriting} \label{sec:rewrite_goals}
 \index{tactics!meta-rewriting|bold}\index{meta-rewriting|bold}
 \index{definitions}
@@ -68,13 +52,10 @@
 
 There are rules for unfolding and folding definitions; Isabelle does not do
 this automatically.  The corresponding tactics rewrite the proof state,
-yielding a single next state.  See also the {\tt goalw} command, which is the
-easiest way of handling definitions.
+yielding a single next state.
 \begin{ttbox} 
 rewrite_goals_tac : thm list -> tactic
-rewrite_tac       : thm list -> tactic
 fold_goals_tac    : thm list -> tactic
-fold_tac          : thm list -> tactic
 \end{ttbox}
 \begin{ttdescription}
 \item[\ttindexbold{rewrite_goals_tac} {\it defs}]  
@@ -82,16 +63,9 @@
 leaving the main goal unchanged.  Use \ttindex{SELECT_GOAL} to restrict it to a
 particular subgoal.
 
-\item[\ttindexbold{rewrite_tac} {\it defs}]  
-unfolds the {\it defs} throughout the proof state, including the main goal
---- not normally desirable!
-
 \item[\ttindexbold{fold_goals_tac} {\it defs}]  
 folds the {\it defs} throughout the subgoals of the proof state, while
 leaving the main goal unchanged.
-
-\item[\ttindexbold{fold_tac} {\it defs}]  
-folds the {\it defs} throughout the proof state.
 \end{ttdescription}
 
 \begin{warn}
diff -r bc874d2ee55a -r 3ba3681d8930 doc-src/Ref/tctical.tex
--- a/doc-src/Ref/tctical.tex	Wed Jan 25 15:39:08 2012 +0100
+++ b/doc-src/Ref/tctical.tex	Wed Jan 25 16:16:20 2012 +0100
@@ -344,16 +344,15 @@
 \index{tacticals!for restriction to a subgoal}
 \begin{ttbox} 
 SELECT_GOAL : tactic -> int -> tactic
-METAHYPS    : (thm list -> 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
-(do not use {\tt rewrite_tac}).  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$}.
+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$
@@ -363,40 +362,8 @@
   SELECT_GOAL} inserts a quantifier to create the state
 \[ (\Forall x.\psi\Imp\theta)\Imp(\Forall x.\psi\Imp\theta). \]
 
-\item[\ttindexbold{METAHYPS} {\it tacf} $i$]\index{meta-assumptions}
-takes subgoal~$i$, of the form 
-\[ \Forall x@1 \ldots x@l. \List{\theta@1; \ldots; \theta@k}\Imp\theta, \]
-and creates the list $\theta'@1$, \ldots, $\theta'@k$ of meta-level
-assumptions.  In these theorems, the subgoal's parameters ($x@1$,
-\ldots,~$x@l$) become free variables.  It supplies the assumptions to
-$tacf$ and applies the resulting tactic to the proof state
-$\theta\Imp\theta$.
-
-If the resulting proof state is $\List{\phi@1; \ldots; \phi@n} \Imp \phi$,
-possibly containing $\theta'@1,\ldots,\theta'@k$ as assumptions, then it is
-lifted back into the original context, yielding $n$ subgoals.
-
-Meta-level assumptions may not contain unknowns.  Unknowns in the
-hypotheses $\theta@1,\ldots,\theta@k$ become free variables in $\theta'@1$,
-\ldots, $\theta'@k$, and are restored afterwards; the {\tt METAHYPS} call
-cannot instantiate them.  Unknowns in $\theta$ may be instantiated.  New
-unknowns in $\phi@1$, \ldots, $\phi@n$ are lifted over the parameters.
-
-Here is a typical application.  Calling {\tt hyp_res_tac}~$i$ resolves
-subgoal~$i$ with one of its own assumptions, which may itself have the form
-of an inference rule (these are called {\bf higher-level assumptions}).  
-\begin{ttbox} 
-val hyp_res_tac = METAHYPS (fn prems => resolve_tac prems 1);
-\end{ttbox} 
-The function \ttindex{gethyps} is useful for debugging applications of {\tt
-  METAHYPS}. 
 \end{ttdescription}
 
-\begin{warn}
-{\tt METAHYPS} fails if the context or new subgoals contain type unknowns.
-In principle, the tactical could treat these like ordinary unknowns.
-\end{warn}
-
 
 \subsection{Scanning for a subgoal by number}
 \index{tacticals!scanning for subgoals}
diff -r bc874d2ee55a -r 3ba3681d8930 doc-src/Ref/thm.tex
--- a/doc-src/Ref/thm.tex	Wed Jan 25 15:39:08 2012 +0100
+++ b/doc-src/Ref/thm.tex	Wed Jan 25 16:16:20 2012 +0100
@@ -143,7 +143,6 @@
 nprems_of     : thm -> int
 tpairs_of     : thm -> (term*term) list
 theory_of_thm : thm -> theory
-dest_state : thm * int -> (term*term) list * term list * term * term
 \end{ttbox}
 \begin{ttdescription}
 \item[\ttindexbold{cprop_of} $thm$] returns the statement of $thm$ as
@@ -169,11 +168,6 @@
   with $thm$.  Note that this does a lookup in Isabelle's global
   database of loaded theories.
 
-\item[\ttindexbold{dest_state} $(thm,i)$] 
-decomposes $thm$ as a tuple containing a list of flex-flex constraints, a
-list of the subgoals~1 to~$i-1$, subgoal~$i$, and the rest of the theorem
-(this will be an implication if there are more than $i$ subgoals).
-
 \end{ttdescription}