src/HOL/Lazy_Sequence.thy

--- a/src/HOL/Lazy_Sequence.thy	Thu May 13 00:44:48 2010 +0200
+++ b/src/HOL/Lazy_Sequence.thy	Wed May 12 22:33:10 2010 -0700
@@ -136,7 +136,7 @@
   datatypes lazy_sequence = Lazy_Sequence
   functions map yield yieldn
 
-section {* With Hit Bound Value *}
+subsection {* With Hit Bound Value *}
 text {* assuming in negative context *}
 
 types 'a hit_bound_lazy_sequence = "'a option lazy_sequence"