author | paulson |
Thu, 10 Dec 2009 17:34:09 +0000 | |
changeset 34054 | 8e07304ecd0c |
parent 33898 | 2ca2693a8c10 |
child 34055 | fdf294ee08b2 |
--- a/doc-src/TutorialI/Rules/rules.tex Wed Nov 25 15:21:41 2009 +0100 +++ b/doc-src/TutorialI/Rules/rules.tex Thu Dec 10 17:34:09 2009 +0000 @@ -1073,7 +1073,7 @@ \index{quantifiers!existential|)} -\subsection{Renaming an Assumption: {\tt\slshape rename_tac}} +\subsection{Renaming a Bound Variable: {\tt\slshape rename_tac}} \index{assumptions!renaming|(}\index{*rename_tac (method)|(}% When you apply a rule such as \isa{allI}, the quantified variable