Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
doc-src/IsarImplementation/Thy/document/Eq.tex
changeset 46486 4a607979290d
parent 46295 2548a85b0e02 
--- 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.
isabelle