# HG changeset patch
# User wenzelm
# Date 1329332145 -3600
# Node ID 4a607979290de909cbe6fe80643517c53bdf995b
# Parent  f584616218393b11459e70ede15a31d129aeaa82
updated rewrite_goals_rule, rewrite_rule;

diff -r f58461621839 -r 4a607979290d doc-src/IsarImplementation/Thy/Eq.thy
--- 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.
 
diff -r f58461621839 -r 4a607979290d doc-src/IsarImplementation/Thy/document/Eq.tex
--- 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.
 
diff -r f58461621839 -r 4a607979290d 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