src/HOL/Lazy_Sequence.thy
changeset 42163 392fd6c4669c
parent 40056 0bee30e3a4ad
child 45214 66ba67adafab
     1.1 --- a/src/HOL/Lazy_Sequence.thy	Wed Mar 30 11:32:51 2011 +0200
     1.2 +++ b/src/HOL/Lazy_Sequence.thy	Wed Mar 30 11:32:52 2011 +0200
     1.3 @@ -208,7 +208,7 @@
     1.4  subsection {* With Hit Bound Value *}
     1.5  text {* assuming in negative context *}
     1.6  
     1.7 -types 'a hit_bound_lazy_sequence = "'a option lazy_sequence"
     1.8 +type_synonym 'a hit_bound_lazy_sequence = "'a option lazy_sequence"
     1.9  
    1.10  definition hit_bound :: "'a hit_bound_lazy_sequence"
    1.11  where