1.1 --- a/doc-src/TutorialI/fp.tex	Sat Nov 04 18:54:22 2000 +0100
     1.2 +++ b/doc-src/TutorialI/fp.tex	Mon Nov 06 11:32:23 2000 +0100
     1.3 @@ -257,7 +257,7 @@
     1.4    \indexboldpos{\isasymle}{$HOL2arithrel} and
     1.5    \ttindexboldpos{<}{$HOL2arithrel} are overloaded, i.e.\ they are available
     1.6    not just for natural numbers but at other types as well (see
     1.7 -  \S\ref{sec:TypeClasses}). For example, given the goal \isa{x+0 = x}, there
     1.8 +  \S\ref{sec:overloading}). For example, given the goal \isa{x+0 = x}, there
     1.9    is nothing to indicate that you are talking about natural numbers.  Hence
    1.10    Isabelle can only infer that \isa{x} is of some arbitrary type where
    1.11    \isa{0} and \isa{+} are declared. As a consequence, you will be unable to
    1.12 @@ -305,7 +305,7 @@
    1.13  \index{arithmetic|)}
    1.14  
    1.15  
    1.16 -\subsection{Products}
    1.17 +\subsection{Pairs}
    1.18  \input{Misc/document/pairs.tex}
    1.19  
    1.20  %FIXME move stuff below into section on proofs about products?
    1.21 @@ -315,16 +315,16 @@
    1.22    of a term may differ, which can affect proofs. If you want to avoid this
    1.23    complication, use \isa{fst} and \isa{snd}, i.e.\ write
    1.24    \isa{\isasymlambda{}p.~fst p + snd p} instead of
    1.25 -  \isa{\isasymlambda(x,y).~x + y}.  See~\S\ref{proofs-about-products} for
    1.26 +  \isa{\isasymlambda(x,y).~x + y}.  See~\S\ref{sec:products} for
    1.27    theorem proving with tuple patterns.
    1.28  \end{warn}
    1.29  
    1.30 -Note that products, like natural numbers, are datatypes, which means
    1.31 +Note that products, like type \isa{nat}, are datatypes, which means
    1.32  in particular that \isa{induct_tac} and \isa{case_tac} are applicable to
    1.33 -products (see \S\ref{proofs-about-products}).
    1.34 +products (see \S\ref{sec:products}).
    1.35  
    1.36  Instead of tuples with many components (where ``many'' is not much above 2),
    1.37 -it is far preferable to use record types (see \S\ref{sec:records}).
    1.38 +it is far preferable to use records (see \S\ref{sec:records}).
    1.39  
    1.40  \section{Definitions}
    1.41  \label{sec:Definitions}