diff -r 1888e3cb8048 -r 262572d90bc6 src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
--- 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