1.1 --- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Sun Jul 04 09:26:30 2010 -0700
     1.2 +++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Mon Jul 05 09:12:35 2010 -0700
     1.3 @@ -3317,7 +3317,7 @@
     1.4  
     1.5  print_antiquotations
     1.6  
     1.7 -section "Instanciate @{typ real} and @{typ complex} as typeclass @{text ordered_euclidean_space}."
     1.8 +subsection "Instantiate @{typ real} and @{typ complex} as typeclass @{text ordered_euclidean_space}."
     1.9  
    1.10  instantiation real :: real_basis_with_inner
    1.11  begin