# HG changeset patch
# User huffman
# Date 1278346355 25200
# Node ID 8c6bfe10a4ae89c740a58d1c6cb7cd62762e1e6e
# Parent  1a24950dae33e43548bdc4b47bd28744290949e4
section -> subsection

diff -r 1a24950dae33 -r 8c6bfe10a4ae src/HOL/Multivariate_Analysis/Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Sun Jul 04 09:26:30 2010 -0700
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Mon Jul 05 09:12:35 2010 -0700
@@ -3317,7 +3317,7 @@
 
 print_antiquotations
 
-section "Instanciate @{typ real} and @{typ complex} as typeclass @{text ordered_euclidean_space}."
+subsection "Instantiate @{typ real} and @{typ complex} as typeclass @{text ordered_euclidean_space}."
 
 instantiation real :: real_basis_with_inner
 begin