equal
deleted
inserted
replaced
1 (* Title: HOL/Analysis/Finite_Cartesian_Product.thy |
1 (* Title: HOL/Analysis/Finite_Cartesian_Product.thy |
2 Author: Amine Chaieb, University of Cambridge |
2 Author: Amine Chaieb, University of Cambridge |
3 *) |
3 *) |
4 |
4 |
5 section%important \<open>Definition of finite Cartesian product types\<close> |
5 section%important \<open>Definition of Finite Cartesian Product Type\<close> |
6 |
6 |
7 theory Finite_Cartesian_Product |
7 theory Finite_Cartesian_Product |
8 imports |
8 imports |
9 Euclidean_Space |
9 Euclidean_Space |
10 L2_Norm |
10 L2_Norm |