doc-src/Ref/thm.tex

--- a/doc-src/Ref/thm.tex	Wed Feb 15 19:31:27 2012 +0100
+++ b/doc-src/Ref/thm.tex	Wed Feb 15 19:55:45 2012 +0100
@@ -9,25 +9,6 @@
 new proof procedures.
 
 
-\section{Basic operations on theorems}
-
-\subsection{Expanding definitions in theorems}
-\index{meta-rewriting!in theorems}
-\begin{ttbox} 
-rewrite_rule       : thm list -> thm -> thm
-rewrite_goals_rule : thm list -> thm -> thm
-\end{ttbox}
-\begin{ttdescription}
-\item[\ttindexbold{rewrite_rule} {\it defs} {\it thm}]  
-unfolds the {\it defs} throughout the theorem~{\it thm}.
-
-\item[\ttindexbold{rewrite_goals_rule} {\it defs} {\it thm}]  
-unfolds the {\it defs} in the premises of~{\it thm}, but it leaves the
-conclusion unchanged.  This rule is the basis for \ttindex{rewrite_goals_tac},
-but it serves little purpose in forward proof.
-\end{ttdescription}
-
-
 \subsection{Instantiating unknowns in a theorem} \label{sec:instantiate}
 \index{instantiation}
 \begin{alltt}\footnotesize