1.1 --- a/doc-src/TutorialI/Misc/pairs.thy	Wed Nov 29 13:44:26 2000 +0100
     1.2 +++ b/doc-src/TutorialI/Misc/pairs.thy	Wed Nov 29 17:23:27 2000 +0100
     1.3 @@ -13,16 +13,21 @@
     1.4  $\tau@1 \times (\tau@2 \times \tau@3)$. Therefore we have
     1.5  \isa{fst(snd($a@1$,$a@2$,$a@3$)) = $a@2$}.
     1.6  
     1.7 +Remarks:
     1.8 +\begin{itemize}
     1.9 +\item
    1.10  There is also the type \isaindexbold{unit}, which contains exactly one
    1.11  element denoted by \ttindexboldpos{()}{$Isatype}. This type can be viewed
    1.12 -as a degenerate Cartesian product of 0 types.
    1.13 -
    1.14 -Note that products, like type @{typ nat}, are datatypes, which means
    1.15 +as a degenerate product with 0 components.
    1.16 +\item
    1.17 +Products, like type @{typ nat}, are datatypes, which means
    1.18  in particular that @{text induct_tac} and @{text case_tac} are applicable to
    1.19 -products (see \S\ref{sec:products}).
    1.20 -
    1.21 +terms of product type.
    1.22 +\item
    1.23  Instead of tuples with many components (where ``many'' is not much above 2),
    1.24 -it is far preferable to use records (see \S\ref{sec:records}).
    1.25 +it is preferable to use records.
    1.26 +\end{itemize}
    1.27 +For more information on pairs and records see Chapter~\ref{ch:more-types}.
    1.28  *}
    1.29  (*<*)
    1.30  end