1.1 --- a/doc-src/TutorialI/Misc/document/simp.tex	Mon Mar 19 13:05:56 2001 +0100
     1.2 +++ b/doc-src/TutorialI/Misc/document/simp.tex	Mon Mar 19 13:28:06 2001 +0100
     1.3 @@ -140,7 +140,7 @@
     1.4  }
     1.5  %
     1.6  \begin{isamarkuptext}%
     1.7 -\index{simplification!with definitions}
     1.8 +\label{sec:Simp-with-Defs}\index{simplification!with definitions}
     1.9  Constant definitions (\S\ref{sec:ConstDefinitions}) can
    1.10  be used as simplification rules, but by default they are not.  Hence the
    1.11  simplifier does not expand them automatically, just as it should be:
    1.12 @@ -238,7 +238,7 @@
    1.13  }
    1.14  %
    1.15  \begin{isamarkuptext}%
    1.16 -\indexbold{case splits}\index{*split (method, attr.)|(}
    1.17 +\label{sec:AutoCaseSplits}\indexbold{case splits}\index{*split (method, attr.)|(}
    1.18  Goals containing \isa{if}-expressions are usually proved by case
    1.19  distinction on the condition of the \isa{if}. For example the goal%
    1.20  \end{isamarkuptext}%

     2.1 --- a/doc-src/TutorialI/Misc/natsum.thy	Mon Mar 19 13:05:56 2001 +0100
     2.2 +++ b/doc-src/TutorialI/Misc/natsum.thy	Mon Mar 19 13:28:06 2001 +0100
     2.3 @@ -59,7 +59,7 @@
     2.4  \end{warn}
     2.5  
     2.6  Simple arithmetic goals are proved automatically by both @{term auto} and the
     2.7 -simplification methods introduced in \S\ref{sec:Simplification}.  For
     2.8 +simplification method introduced in \S\ref{sec:Simplification}.  For
     2.9  example,
    2.10  *}
    2.11  

     3.1 --- a/doc-src/TutorialI/Misc/simp.thy	Mon Mar 19 13:05:56 2001 +0100
     3.2 +++ b/doc-src/TutorialI/Misc/simp.thy	Mon Mar 19 13:28:06 2001 +0100
     3.3 @@ -135,7 +135,7 @@
     3.4  
     3.5  subsection{*Rewriting with Definitions*}
     3.6  
     3.7 -text{*\index{simplification!with definitions}
     3.8 +text{*\label{sec:Simp-with-Defs}\index{simplification!with definitions}
     3.9  Constant definitions (\S\ref{sec:ConstDefinitions}) can
    3.10  be used as simplification rules, but by default they are not.  Hence the
    3.11  simplifier does not expand them automatically, just as it should be:
    3.12 @@ -237,7 +237,7 @@
    3.13  
    3.14  subsection{*Automatic Case Splits*}
    3.15  
    3.16 -text{*\indexbold{case splits}\index{*split (method, attr.)|(}
    3.17 +text{*\label{sec:AutoCaseSplits}\indexbold{case splits}\index{*split (method, attr.)|(}
    3.18  Goals containing @{text"if"}-expressions are usually proved by case
    3.19  distinction on the condition of the @{text"if"}. For example the goal
    3.20  *}

     4.1 --- a/doc-src/TutorialI/Recdef/document/simplification.tex	Mon Mar 19 13:05:56 2001 +0100
     4.2 +++ b/doc-src/TutorialI/Recdef/document/simplification.tex	Mon Mar 19 13:28:06 2001 +0100
     4.3 @@ -44,11 +44,10 @@
     4.4  simplification steps. Fortunately, this problem can be avoided in many
     4.5  different ways.
     4.6  
     4.7 -The most radical solution is to disable the offending
     4.8 -\isa{split{\isacharunderscore}if} as shown in the section on case splits in
     4.9 -\S\ref{sec:Simplification}.  However, we do not recommend this because it
    4.10 -means you will often have to invoke the rule explicitly when \isa{if} is
    4.11 -involved.
    4.12 +The most radical solution is to disable the offending \isa{split{\isacharunderscore}if}
    4.13 +as shown in \S\ref{sec:AutoCaseSplits}.  However, we do not recommend this
    4.14 +because it means you will often have to invoke the rule explicitly when
    4.15 +\isa{if} is involved.
    4.16  
    4.17  If possible, the definition should be given by pattern matching on the left
    4.18  rather than \isa{if} on the right. In the case of \isa{gcd} the

     5.1 --- a/doc-src/TutorialI/Recdef/simplification.thy	Mon Mar 19 13:05:56 2001 +0100
     5.2 +++ b/doc-src/TutorialI/Recdef/simplification.thy	Mon Mar 19 13:28:06 2001 +0100
     5.3 @@ -37,11 +37,10 @@
     5.4  simplification steps. Fortunately, this problem can be avoided in many
     5.5  different ways.
     5.6  
     5.7 -The most radical solution is to disable the offending
     5.8 -@{thm[source]split_if} as shown in the section on case splits in
     5.9 -\S\ref{sec:Simplification}.  However, we do not recommend this because it
    5.10 -means you will often have to invoke the rule explicitly when @{text if} is
    5.11 -involved.
    5.12 +The most radical solution is to disable the offending @{thm[source]split_if}
    5.13 +as shown in \S\ref{sec:AutoCaseSplits}.  However, we do not recommend this
    5.14 +because it means you will often have to invoke the rule explicitly when
    5.15 +@{text if} is involved.
    5.16  
    5.17  If possible, the definition should be given by pattern matching on the left
    5.18  rather than @{text if} on the right. In the case of @{term gcd} the

     6.1 --- a/doc-src/TutorialI/fp.tex	Mon Mar 19 13:05:56 2001 +0100
     6.2 +++ b/doc-src/TutorialI/fp.tex	Mon Mar 19 13:28:06 2001 +0100
     6.3 @@ -263,7 +263,7 @@
     6.4  
     6.5  Note that pattern-matching is not allowed, i.e.\ each definition must be of
     6.6  the form $f\,x@1\,\dots\,x@n~\isasymequiv~t$.
     6.7 -Section~{\S}\ref{sec:Simplification} explains how definitions are used
     6.8 +Section~{\S}\ref{sec:Simp-with-Defs} explains how definitions are used
     6.9  in proofs.
    6.10  
    6.11  \input{Misc/document/prime_def.tex}