equal
deleted
inserted
replaced
3 *) |
3 *) |
4 |
4 |
5 header {* Definition of finite Cartesian product types. *} |
5 header {* Definition of finite Cartesian product types. *} |
6 |
6 |
7 theory Finite_Cartesian_Product |
7 theory Finite_Cartesian_Product |
8 imports Inner_Product L2_Norm Numeral_Type |
8 imports |
|
9 "~~/src/HOL/Library/Inner_Product" |
|
10 L2_Norm |
|
11 "~~/src/HOL/Library/Numeral_Type" |
9 begin |
12 begin |
10 |
13 |
11 subsection {* Finite Cartesian products, with indexing and lambdas. *} |
14 subsection {* Finite Cartesian products, with indexing and lambdas. *} |
12 |
15 |
13 typedef (open Cart) |
16 typedef (open Cart) |