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