src/HOL/Library/Finite_Cartesian_Product.thy

--- a/src/HOL/Library/Finite_Cartesian_Product.thy	Fri Feb 13 14:41:54 2009 -0800
+++ b/src/HOL/Library/Finite_Cartesian_Product.thy	Fri Feb 13 14:45:10 2009 -0800
@@ -33,7 +33,7 @@
 by (simp add: dimindex_def hassize_def)
 
 
-section{* An indexing type parametrized by base type. *}
+subsection{* An indexing type parametrized by base type. *}
 
 typedef 'a finite_image = "{1 .. DIM('a)}"
   using dimindex_ge_1 by auto