equal
deleted
inserted
replaced
1 (* Title: HOL/ex/Tuple.thy |
1 (* Title: HOL/ex/Tuple.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Markus Wenzel, TU Muenchen |
3 Author: Markus Wenzel, TU Muenchen |
4 |
|
5 Properly nested products (see also theory Prod). |
|
6 |
|
7 Unquestionably, this should be used as the standard representation of |
|
8 tuples in HOL, but it breaks many existing theories! |
|
9 *) |
4 *) |
10 |
5 |
11 header {* Properly nested products *} |
6 header {* Properly nested products *} |
12 |
7 |
13 theory Tuple imports HOL begin |
8 theory Tuple imports HOL begin |