--- 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}%