--- a/doc-src/IsarImplementation/Thy/Eq.thy Wed Feb 15 19:31:27 2012 +0100
+++ b/doc-src/IsarImplementation/Thy/Eq.thy Wed Feb 15 19:55:45 2012 +0100
@@ -50,6 +50,8 @@
text %mlref {*
\begin{mldecls}
+ @{index_ML rewrite_rule: "thm list -> thm -> thm"} \\
+ @{index_ML rewrite_goals_rule: "thm list -> thm -> thm"} \\
@{index_ML rewrite_goal_tac: "thm list -> int -> tactic"} \\
@{index_ML rewrite_goals_tac: "thm list -> tactic"} \\
@{index_ML fold_goals_tac: "thm list -> tactic"} \\
@@ -57,6 +59,14 @@
\begin{description}
+ \item @{ML rewrite_rule}~@{text "rules thm"} rewrites the whole
+ theorem by the given rules.
+
+ \item @{ML rewrite_goals_rule}~@{text "rules thm"} rewrites the
+ outer premises of the given theorem. Interpreting the same as a
+ goal state (\secref{sec:tactical-goals}) it means to rewrite all
+ subgoals (in the same manner as @{ML rewrite_goals_tac}).
+
\item @{ML rewrite_goal_tac}~@{text "rules i"} rewrites subgoal
@{text "i"} by the given rewrite rules.
--- a/doc-src/IsarImplementation/Thy/document/Eq.tex Wed Feb 15 19:31:27 2012 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Eq.tex Wed Feb 15 19:55:45 2012 +0100
@@ -86,6 +86,8 @@
%
\begin{isamarkuptext}%
\begin{mldecls}
+ \indexdef{}{ML}{rewrite\_rule}\verb|rewrite_rule: thm list -> thm -> thm| \\
+ \indexdef{}{ML}{rewrite\_goals\_rule}\verb|rewrite_goals_rule: thm list -> thm -> thm| \\
\indexdef{}{ML}{rewrite\_goal\_tac}\verb|rewrite_goal_tac: thm list -> int -> tactic| \\
\indexdef{}{ML}{rewrite\_goals\_tac}\verb|rewrite_goals_tac: thm list -> tactic| \\
\indexdef{}{ML}{fold\_goals\_tac}\verb|fold_goals_tac: thm list -> tactic| \\
@@ -93,6 +95,14 @@
\begin{description}
+ \item \verb|rewrite_rule|~\isa{rules\ thm} rewrites the whole
+ theorem by the given rules.
+
+ \item \verb|rewrite_goals_rule|~\isa{rules\ thm} rewrites the
+ outer premises of the given theorem. Interpreting the same as a
+ goal state (\secref{sec:tactical-goals}) it means to rewrite all
+ subgoals (in the same manner as \verb|rewrite_goals_tac|).
+
\item \verb|rewrite_goal_tac|~\isa{rules\ i} rewrites subgoal
\isa{i} by the given rewrite rules.
--- 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