--- a/doc-src/TutorialI/Misc/simp.thy Thu Dec 13 16:48:07 2001 +0100
+++ b/doc-src/TutorialI/Misc/simp.thy Thu Dec 13 16:48:34 2001 +0100
@@ -21,7 +21,7 @@
are explained in \S\ref{sec:SimpHow}.
The simplification attribute of theorems can be turned on and off:%
-\index{*simp del (attribute)}\REMARK{need to index attributes!switching off??}
+\index{*simp del (attribute)}
\begin{quote}
\isacommand{declare} \textit{theorem-name}@{text"[simp]"}\\
\isacommand{declare} \textit{theorem-name}@{text"[simp del]"}