diff -r 3b3cc0cf533f -r b44ad7e4c4d2 doc-src/TutorialI/Misc/document/simp.tex
--- a/doc-src/TutorialI/Misc/document/simp.tex	Mon Mar 19 13:05:56 2001 +0100
+++ b/doc-src/TutorialI/Misc/document/simp.tex	Mon Mar 19 13:28:06 2001 +0100
@@ -140,7 +140,7 @@
 }
 %
 \begin{isamarkuptext}%
-\index{simplification!with definitions}
+\label{sec:Simp-with-Defs}\index{simplification!with definitions}
 Constant definitions (\S\ref{sec:ConstDefinitions}) can
 be used as simplification rules, but by default they are not.  Hence the
 simplifier does not expand them automatically, just as it should be:
@@ -238,7 +238,7 @@
 }
 %
 \begin{isamarkuptext}%
-\indexbold{case splits}\index{*split (method, attr.)|(}
+\label{sec:AutoCaseSplits}\indexbold{case splits}\index{*split (method, attr.)|(}
 Goals containing \isa{if}-expressions are usually proved by case
 distinction on the condition of the \isa{if}. For example the goal%
 \end{isamarkuptext}%