diff -r f9a1cd2599dd -r 2548a85b0e02 doc-src/Ref/tactic.tex
--- a/doc-src/Ref/tactic.tex	Tue Feb 07 18:56:40 2012 +0100
+++ b/doc-src/Ref/tactic.tex	Thu Feb 09 19:34:23 2012 +0100
@@ -29,44 +29,6 @@
 \end{ttdescription}
 
 
-\subsection{Definitions and meta-level rewriting} \label{sec:rewrite_goals}
-\index{tactics!meta-rewriting|bold}\index{meta-rewriting|bold}
-\index{definitions}
-
-Definitions in Isabelle have the form $t\equiv u$, where $t$ is typically a
-constant or a constant applied to a list of variables, for example $\it
-sqr(n)\equiv n\times n$.  Conditional definitions, $\phi\Imp t\equiv u$,
-are also supported.  {\bf Unfolding} the definition ${t\equiv u}$ means using
-it as a rewrite rule, replacing~$t$ by~$u$ throughout a theorem.  {\bf
-Folding} $t\equiv u$ means replacing~$u$ by~$t$.  Rewriting continues until
-no rewrites are applicable to any subterm.
-
-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.
-\begin{ttbox} 
-rewrite_goals_tac : thm list -> tactic
-fold_goals_tac    : thm list -> tactic
-\end{ttbox}
-\begin{ttdescription}
-\item[\ttindexbold{rewrite_goals_tac} {\it defs}]  
-unfolds the {\it defs} throughout the subgoals of the proof state, while
-leaving the main goal unchanged.  Use \ttindex{SELECT_GOAL} to restrict it to a
-particular subgoal.
-
-\item[\ttindexbold{fold_goals_tac} {\it defs}]  
-folds the {\it defs} throughout the subgoals of the proof state, while
-leaving the main goal unchanged.
-\end{ttdescription}
-
-\begin{warn}
-  These tactics only cope with definitions expressed as meta-level
-  equalities ($\equiv$).  More general equivalences are handled by the
-  simplifier, provided that it is set up appropriately for your logic
-  (see Chapter~\ref{chap:simplification}).
-\end{warn}
-
-
 \subsection{Composition: resolution without lifting}
 \index{tactics!for composition}
 \begin{ttbox}