--- a/doc-src/TutorialI/Misc/document/pairs.tex Wed Nov 29 10:22:38 2000 +0100
+++ b/doc-src/TutorialI/Misc/document/pairs.tex Wed Nov 29 13:44:26 2000 +0100
@@ -3,25 +3,28 @@
\def\isabellecontext{pairs}%
%
\begin{isamarkuptext}%
+\label{sec:pairs}\indexbold{product type}
+\index{pair|see{product type}}\index{tuple|see{product type}}
HOL also has pairs: \isa{($a@1$,$a@2$)} is of type $\tau@1$
-\indexboldpos{\isasymtimes}{$IsaFun} $\tau@2$ provided each $a@i$ is of type
-$\tau@i$. The components of a pair are extracted by \isa{fst} and
-\isa{snd}: \isa{fst($x$,$y$) = $x$} and \isa{snd($x$,$y$) = $y$}. Tuples
+\indexboldpos{\isasymtimes}{$Isatype} $\tau@2$ provided each $a@i$ is of type
+$\tau@i$. The components of a pair are extracted by \isaindexbold{fst} and
+\isaindexbold{snd}:
+ \isa{fst($x$,$y$) = $x$} and \isa{snd($x$,$y$) = $y$}. Tuples
are simulated by pairs nested to the right: \isa{($a@1$,$a@2$,$a@3$)} stands
for \isa{($a@1$,($a@2$,$a@3$))} and $\tau@1 \times \tau@2 \times \tau@3$ for
$\tau@1 \times (\tau@2 \times \tau@3)$. Therefore we have
\isa{fst(snd($a@1$,$a@2$,$a@3$)) = $a@2$}.
-It is possible to use (nested) tuples as patterns in abstractions, for
-example \isa{\isasymlambda(x,y,z).x+y+z} and
-\isa{\isasymlambda((x,y),z).x+y+z}.
-In addition to explicit $\lambda$-abstractions, tuple patterns can be used in
-most variable binding constructs. Typical examples are
-\begin{quote}
-\isa{let\ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isacharequal}\ f\ z\ in\ {\isacharparenleft}y{\isacharcomma}\ x{\isacharparenright}}\\
-\isa{case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ {\isadigit{0}}\ {\isacharbar}\ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isacharhash}\ zs\ {\isasymRightarrow}\ x\ {\isacharplus}\ y}
-\end{quote}
-Further important examples are quantifiers and sets (see~\S\ref{quant-pats}).%
+There is also the type \isaindexbold{unit}, which contains exactly one
+element denoted by \ttindexboldpos{()}{$Isatype}. This type can be viewed
+as a degenerate Cartesian product of 0 types.
+
+Note that products, like type \isa{nat}, are datatypes, which means
+in particular that \isa{induct{\isacharunderscore}tac} and \isa{case{\isacharunderscore}tac} are applicable to
+products (see \S\ref{sec:products}).
+
+Instead of tuples with many components (where ``many'' is not much above 2),
+it is far preferable to use records (see \S\ref{sec:records}).%
\end{isamarkuptext}%
\end{isabellebody}%
%%% Local Variables: