--- 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}%
--- a/doc-src/TutorialI/Misc/natsum.thy Mon Mar 19 13:05:56 2001 +0100
+++ b/doc-src/TutorialI/Misc/natsum.thy Mon Mar 19 13:28:06 2001 +0100
@@ -59,7 +59,7 @@
\end{warn}
Simple arithmetic goals are proved automatically by both @{term auto} and the
-simplification methods introduced in \S\ref{sec:Simplification}. For
+simplification method introduced in \S\ref{sec:Simplification}. For
example,
*}
--- a/doc-src/TutorialI/Misc/simp.thy Mon Mar 19 13:05:56 2001 +0100
+++ b/doc-src/TutorialI/Misc/simp.thy Mon Mar 19 13:28:06 2001 +0100
@@ -135,7 +135,7 @@
subsection{*Rewriting with Definitions*}
-text{*\index{simplification!with definitions}
+text{*\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:
@@ -237,7 +237,7 @@
subsection{*Automatic Case Splits*}
-text{*\indexbold{case splits}\index{*split (method, attr.)|(}
+text{*\label{sec:AutoCaseSplits}\indexbold{case splits}\index{*split (method, attr.)|(}
Goals containing @{text"if"}-expressions are usually proved by case
distinction on the condition of the @{text"if"}. For example the goal
*}
--- a/doc-src/TutorialI/Recdef/document/simplification.tex Mon Mar 19 13:05:56 2001 +0100
+++ b/doc-src/TutorialI/Recdef/document/simplification.tex Mon Mar 19 13:28:06 2001 +0100
@@ -44,11 +44,10 @@
simplification steps. Fortunately, this problem can be avoided in many
different ways.
-The most radical solution is to disable the offending
-\isa{split{\isacharunderscore}if} as shown in the section on case splits in
-\S\ref{sec:Simplification}. However, we do not recommend this because it
-means you will often have to invoke the rule explicitly when \isa{if} is
-involved.
+The most radical solution is to disable the offending \isa{split{\isacharunderscore}if}
+as shown in \S\ref{sec:AutoCaseSplits}. However, we do not recommend this
+because it means you will often have to invoke the rule explicitly when
+\isa{if} is involved.
If possible, the definition should be given by pattern matching on the left
rather than \isa{if} on the right. In the case of \isa{gcd} the
--- a/doc-src/TutorialI/Recdef/simplification.thy Mon Mar 19 13:05:56 2001 +0100
+++ b/doc-src/TutorialI/Recdef/simplification.thy Mon Mar 19 13:28:06 2001 +0100
@@ -37,11 +37,10 @@
simplification steps. Fortunately, this problem can be avoided in many
different ways.
-The most radical solution is to disable the offending
-@{thm[source]split_if} as shown in the section on case splits in
-\S\ref{sec:Simplification}. However, we do not recommend this because it
-means you will often have to invoke the rule explicitly when @{text if} is
-involved.
+The most radical solution is to disable the offending @{thm[source]split_if}
+as shown in \S\ref{sec:AutoCaseSplits}. However, we do not recommend this
+because it means you will often have to invoke the rule explicitly when
+@{text if} is involved.
If possible, the definition should be given by pattern matching on the left
rather than @{text if} on the right. In the case of @{term gcd} the
--- a/doc-src/TutorialI/fp.tex Mon Mar 19 13:05:56 2001 +0100
+++ b/doc-src/TutorialI/fp.tex Mon Mar 19 13:28:06 2001 +0100
@@ -263,7 +263,7 @@
Note that pattern-matching is not allowed, i.e.\ each definition must be of
the form $f\,x@1\,\dots\,x@n~\isasymequiv~t$.
-Section~{\S}\ref{sec:Simplification} explains how definitions are used
+Section~{\S}\ref{sec:Simp-with-Defs} explains how definitions are used
in proofs.
\input{Misc/document/prime_def.tex}