changeset 17914 | 99ead7a7eb42 |
parent 15905 | 0a4cc9b113c7 |
child 27027 | 63f0b638355c |
17913:4159e1523ad8 | 17914:99ead7a7eb42 |
---|---|
1 (*<*)theory Pairs = Main:(*>*) |
1 (*<*)theory Pairs imports Main begin(*>*) |
2 |
2 |
3 section{*Pairs and Tuples*} |
3 section{*Pairs and Tuples*} |
4 |
4 |
5 text{*\label{sec:products} |
5 text{*\label{sec:products} |
6 Ordered pairs were already introduced in \S\ref{sec:pairs}, but only with a minimal |
6 Ordered pairs were already introduced in \S\ref{sec:pairs}, but only with a minimal |