src/HOL/Lazy_Sequence.thy
changeset 36176 3fe7e97ccca8
parent 36049 0ce5b7a5c2fd
child 36513 70096cbdd4e0
     1.1 --- a/src/HOL/Lazy_Sequence.thy	Fri Apr 16 20:56:40 2010 +0200
     1.2 +++ b/src/HOL/Lazy_Sequence.thy	Fri Apr 16 21:28:09 2010 +0200
     1.3 @@ -212,8 +212,8 @@
     1.4  where
     1.5    "hb_not_seq xq = (case yield xq of None => single () | Some (x, xq) => empty)"
     1.6  
     1.7 -hide (open) type lazy_sequence
     1.8 -hide (open) const Empty Insert Lazy_Sequence yield empty single append flat map bind if_seq iterate_upto not_seq
     1.9 -hide fact yield.simps empty_def single_def append.simps flat.simps map.simps bind_def iterate_upto.simps if_seq_def not_seq_def
    1.10 +hide_type (open) lazy_sequence
    1.11 +hide_const (open) Empty Insert Lazy_Sequence yield empty single append flat map bind if_seq iterate_upto not_seq
    1.12 +hide_fact yield.simps empty_def single_def append.simps flat.simps map.simps bind_def iterate_upto.simps if_seq_def not_seq_def
    1.13  
    1.14  end