| changeset 58877 | 262572d90bc6 |
| parent 57865 | dcfb33c26f50 |
| child 60420 | 884f54e01427 |
--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Sun Nov 02 17:06:05 2014 +0100 +++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Sun Nov 02 17:09:04 2014 +0100 @@ -1,4 +1,4 @@ -header {*Instanciates the finite cartesian product of euclidean spaces as a euclidean space.*} +section {*Instanciates the finite cartesian product of euclidean spaces as a euclidean space.*} theory Cartesian_Euclidean_Space imports Finite_Cartesian_Product Integration