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 License: GPL (GNU GENERAL PUBLIC LICENSE) |
|
5 |
4 |
6 Properly nested products (see also theory Prod). |
5 Properly nested products (see also theory Prod). |
7 |
6 |
8 Unquestionably, this should be used as the standard representation of |
7 Unquestionably, this should be used as the standard representation of |
9 tuples in HOL, but it breaks many existing theories! |
8 tuples in HOL, but it breaks many existing theories! |