| changeset 50055 | 94041d602ecb |
| parent 42163 | 392fd6c4669c |
--- a/src/HOL/New_DSequence.thy Mon Nov 12 18:42:49 2012 +0100 +++ b/src/HOL/New_DSequence.thy Mon Nov 12 23:24:40 2012 +0100 @@ -4,7 +4,7 @@ header {* Depth-Limited Sequences with failure element *} theory New_DSequence -imports Random_Sequence +imports DSequence begin subsection {* Positive Depth-Limited Sequence *}