1.1 --- a/doc-src/TutorialI/Misc/pairs.thy	Fri Aug 04 23:02:11 2000 +0200
     1.2 +++ b/doc-src/TutorialI/Misc/pairs.thy	Sun Aug 06 15:26:53 2000 +0200
     1.3 @@ -1,8 +1,26 @@
     1.4  (*<*)
     1.5  theory pairs = Main:;
     1.6 -term(*>*) "let (x,y) = f z in (y,x)";
     1.7 +(*>*)
     1.8 +text{*
     1.9 +HOL also has pairs: \isa{($a@1$,$a@2$)} is of type \isa{$\tau@1$ *
    1.10 +  $\tau@2$} provided each $a@i$ is of type $\tau@i$. The components of a pair
    1.11 +are extracted by \isa{fst} and \isa{snd}: \isa{fst($x$,$y$) = $x$} and
    1.12 +\isa{snd($x$,$y$) = $y$}. Tuples are simulated by pairs nested to the right:
    1.13 +\isa{($a@1$,$a@2$,$a@3$)} stands for \isa{($a@1$,($a@2$,$a@3$))} and
    1.14 +\isa{$\tau@1$ * $\tau@2$ * $\tau@3$} for \isa{$\tau@1$ * ($\tau@2$ *
    1.15 +  $\tau@3$)}. Therefore we have \isa{fst(snd($a@1$,$a@2$,$a@3$)) = $a@2$}.
    1.16 +
    1.17 +It is possible to use (nested) tuples as patterns in abstractions, for
    1.18 +example \isa{\isasymlambda(x,y,z).x+y+z} and
    1.19 +\isa{\isasymlambda((x,y),z).x+y+z}.
    1.20 +In addition to explicit $\lambda$-abstractions, tuple patterns can be used in
    1.21 +most variable binding constructs. Typical examples are
    1.22 +\begin{quote}
    1.23 +@{term"let (x,y) = f z in (y,x)"}\\
    1.24 +@{term"case xs of [] => 0 | (x,y)#zs => x+y"}
    1.25 +\end{quote}
    1.26 +Further important examples are quantifiers and sets (see~\S\ref{quant-pats}).
    1.27 +*}
    1.28  (*<*)
    1.29 -term(*>*) "case xs of [] \\<Rightarrow> 0 | (x,y)#zs \\<Rightarrow> x+y"
    1.30 -(**)(*<*)
    1.31  end
    1.32  (*>*)