| changeset 16417 | 9bc16273c2d4 |
| parent 14981 | e73f8140af78 |
| child 17388 | 495c799df31d |
| 16416:6061ae1f90f2 | 16417:9bc16273c2d4 |
|---|---|
8 tuples in HOL, but it breaks many existing theories! |
8 tuples in HOL, but it breaks many existing theories! |
9 *) |
9 *) |
10 |
10 |
11 header {* Properly nested products *} |
11 header {* Properly nested products *} |
12 |
12 |
13 theory Tuple = HOL: |
13 theory Tuple imports HOL begin |
14 |
14 |
15 |
15 |
16 subsection {* Abstract syntax *} |
16 subsection {* Abstract syntax *} |
17 |
17 |
18 typedecl unit |
18 typedecl unit |