--- 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}