src/HOL/Lazy_Sequence.thy
changeset 36902 c6bae4456741
parent 36533 f8df589ca2a5
child 38857 97775f3e8722
     1.1 --- a/src/HOL/Lazy_Sequence.thy	Thu May 13 00:44:48 2010 +0200
     1.2 +++ b/src/HOL/Lazy_Sequence.thy	Wed May 12 22:33:10 2010 -0700
     1.3 @@ -136,7 +136,7 @@
     1.4    datatypes lazy_sequence = Lazy_Sequence
     1.5    functions map yield yieldn
     1.6  
     1.7 -section {* With Hit Bound Value *}
     1.8 +subsection {* With Hit Bound Value *}
     1.9  text {* assuming in negative context *}
    1.10  
    1.11  types 'a hit_bound_lazy_sequence = "'a option lazy_sequence"