--- a/src/HOL/New_DSequence.thy Thu May 13 00:44:48 2010 +0200
+++ b/src/HOL/New_DSequence.thy Wed May 12 22:33:10 2010 -0700
@@ -7,7 +7,7 @@
imports Random_Sequence
begin
-section {* Positive Depth-Limited Sequence *}
+subsection {* Positive Depth-Limited Sequence *}
types 'a pos_dseq = "code_numeral => 'a Lazy_Sequence.lazy_sequence"
@@ -43,7 +43,7 @@
where
"pos_map f xq = (%i. Lazy_Sequence.map f (xq i))"
-section {* Negative Depth-Limited Sequence *}
+subsection {* Negative Depth-Limited Sequence *}
types 'a neg_dseq = "code_numeral => 'a Lazy_Sequence.hit_bound_lazy_sequence"
@@ -79,7 +79,7 @@
where
"neg_map f xq = (%i. Lazy_Sequence.hb_map f (xq i))"
-section {* Negation *}
+subsection {* Negation *}
definition pos_not_seq :: "unit neg_dseq => unit pos_dseq"
where