equal
deleted
inserted
replaced
1 % |
1 % |
2 \begin{isabellebody}% |
2 \begin{isabellebody}% |
|
3 \def\isabellecontext{pairs}% |
3 % |
4 % |
4 \begin{isamarkuptext}% |
5 \begin{isamarkuptext}% |
5 HOL also has pairs: \isa{($a@1$,$a@2$)} is of type \isa{$\tau@1$ * |
6 HOL also has pairs: \isa{($a@1$,$a@2$)} is of type \isa{$\tau@1$ * |
6 $\tau@2$} provided each $a@i$ is of type $\tau@i$. The components of a pair |
7 $\tau@2$} provided each $a@i$ is of type $\tau@i$. The components of a pair |
7 are extracted by \isa{fst} and \isa{snd}: \isa{fst($x$,$y$) = $x$} and |
8 are extracted by \isa{fst} and \isa{snd}: \isa{fst($x$,$y$) = $x$} and |