--- a/doc-src/TutorialI/Rules/rules.tex Wed Jul 11 17:55:46 2001 +0200
+++ b/doc-src/TutorialI/Rules/rules.tex Thu Jul 12 16:33:36 2001 +0200
@@ -855,7 +855,7 @@
\section{Quantifiers}
-\index{quantifiers|(}\index{quantifiers!universal|(}%
+\index{quantifiers!universal|(}%
Quantifiers require formalizing syntactic substitution and the notion of
arbitrary value. Consider the universal quantifier. In a logic
book, its introduction rule looks like this:
@@ -1035,7 +1035,7 @@
\emph{Hint}: the proof is similar
to the one just above for the universal quantifier.
\end{exercise}
-\index{quantifiers|)}\index{quantifiers!existential|)}
+\index{quantifiers!existential|)}
\subsection{Renaming an Assumption: {\tt\slshape rename_tac}}