src/HOL/New_DSequence.thy
changeset 42163 392fd6c4669c
parent 40049 75d9f57123d6
child 50055 94041d602ecb
     1.1 --- a/src/HOL/New_DSequence.thy	Wed Mar 30 11:32:51 2011 +0200
     1.2 +++ b/src/HOL/New_DSequence.thy	Wed Mar 30 11:32:52 2011 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4  
     1.5  subsection {* Positive Depth-Limited Sequence *}
     1.6  
     1.7 -types 'a pos_dseq = "code_numeral => 'a Lazy_Sequence.lazy_sequence"
     1.8 +type_synonym 'a pos_dseq = "code_numeral => 'a Lazy_Sequence.lazy_sequence"
     1.9  
    1.10  definition pos_empty :: "'a pos_dseq"
    1.11  where
    1.12 @@ -49,7 +49,7 @@
    1.13  
    1.14  subsection {* Negative Depth-Limited Sequence *}
    1.15  
    1.16 -types 'a neg_dseq = "code_numeral => 'a Lazy_Sequence.hit_bound_lazy_sequence"
    1.17 +type_synonym 'a neg_dseq = "code_numeral => 'a Lazy_Sequence.hit_bound_lazy_sequence"
    1.18  
    1.19  definition neg_empty :: "'a neg_dseq"
    1.20  where