# HG changeset patch
# User nipkow
# Date 985004886 -3600
# Node ID b44ad7e4c4d26c9b208ff376d91e3c9e8bd3ca6c
# Parent  3b3cc0cf533f8eb664f6950cc7f7b312d716d51a
*** empty log message ***

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}%
diff -r 3b3cc0cf533f -r b44ad7e4c4d2 doc-src/TutorialI/Misc/natsum.thy
--- 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,
 *}
 
diff -r 3b3cc0cf533f -r b44ad7e4c4d2 doc-src/TutorialI/Misc/simp.thy
--- 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
 *}
diff -r 3b3cc0cf533f -r b44ad7e4c4d2 doc-src/TutorialI/Recdef/document/simplification.tex
--- 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
diff -r 3b3cc0cf533f -r b44ad7e4c4d2 doc-src/TutorialI/Recdef/simplification.thy
--- 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
diff -r 3b3cc0cf533f -r b44ad7e4c4d2 doc-src/TutorialI/fp.tex
--- 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}