src/HOL/New_DSequence.thy

 imports Random_Sequence
 begin
 
 subsection {* Positive Depth-Limited Sequence *}
 
-types 'a pos_dseq = "code_numeral => 'a Lazy_Sequence.lazy_sequence"
+type_synonym 'a pos_dseq = "code_numeral => 'a Lazy_Sequence.lazy_sequence"
 
 definition pos_empty :: "'a pos_dseq"
 where
   "pos_empty = (%i. Lazy_Sequence.empty)"
 

 where
   "pos_map f xq = (%i. Lazy_Sequence.map f (xq i))"
 
 subsection {* Negative Depth-Limited Sequence *}
 
-types 'a neg_dseq = "code_numeral => 'a Lazy_Sequence.hit_bound_lazy_sequence"
+type_synonym 'a neg_dseq = "code_numeral => 'a Lazy_Sequence.hit_bound_lazy_sequence"
 
 definition neg_empty :: "'a neg_dseq"
 where
   "neg_empty = (%i. Lazy_Sequence.empty)"