correctly hiding facts of Lazy_Sequence
authorbulwahn
Fri Jan 22 11:42:28 2010 +0100 (2010-01-22)
changeset 349573b1957113753
parent 34956 fac9d0311725
child 34958 dcd0fa5cc6d3
correctly hiding facts of Lazy_Sequence
src/HOL/Lazy_Sequence.thy
     1.1 --- a/src/HOL/Lazy_Sequence.thy	Thu Jan 21 14:13:21 2010 +0100
     1.2 +++ b/src/HOL/Lazy_Sequence.thy	Fri Jan 22 11:42:28 2010 +0100
     1.3 @@ -153,6 +153,6 @@
     1.4  
     1.5  hide (open) type lazy_sequence
     1.6  hide (open) const Empty Insert Lazy_Sequence yield yieldn empty single append flat map bind if_seq not_seq
     1.7 -hide (open) fact yield.simps yieldn.simps empty_def single_def append.simps flat.simps map.simps bind_def if_seq_def not_seq_def
     1.8 +hide fact yield.simps yieldn.simps empty_def single_def append.simps flat.simps map.simps bind_def if_seq_def not_seq_def
     1.9  
    1.10  end