equal
deleted
inserted
replaced
1 (*<*) |
1 (*<*) |
2 theory pairs2 imports Main begin; |
2 theory pairs2 imports Main begin |
3 (*>*) |
3 (*>*) |
4 text{*\label{sec:pairs}\index{pairs and tuples} |
4 text{*\label{sec:pairs}\index{pairs and tuples} |
5 HOL also has ordered pairs: \isa{($a@1$,$a@2$)} is of type $\tau@1$ |
5 HOL also has ordered pairs: \isa{($a@1$,$a@2$)} is of type $\tau@1$ |
6 \indexboldpos{\isasymtimes}{$Isatype} $\tau@2$ provided each $a@i$ is of type |
6 \indexboldpos{\isasymtimes}{$Isatype} $\tau@2$ provided each $a@i$ is of type |
7 $\tau@i$. The functions \cdx{fst} and |
7 $\tau@i$. The functions \cdx{fst} and |