diff -r 1888e3cb8048 -r 262572d90bc6 src/HOL/Multivariate_Analysis/Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Sun Nov 02 17:06:05 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Sun Nov 02 17:09:04 2014 +0100
@@ -3,7 +3,7 @@
     Author:     Brian Huffman, Portland State University
 *)
 
-header {* Finite-Dimensional Inner Product Spaces *}
+section {* Finite-Dimensional Inner Product Spaces *}
 
 theory Euclidean_Space
 imports