src/HOL/Random_Sequence.thy
changeset 34953 a053ad2a7a72
parent 34948 2d5f2a9f7601
child 36176 3fe7e97ccca8
     1.1 --- a/src/HOL/Random_Sequence.thy	Wed Jan 20 18:02:22 2010 +0100
     1.2 +++ b/src/HOL/Random_Sequence.thy	Wed Jan 20 18:08:08 2010 +0100
     1.3 @@ -56,6 +56,6 @@
     1.4  hide (open) const empty single bind union if_random_dseq not_random_dseq Random map
     1.5  
     1.6  hide type DSequence.dseq random_dseq
     1.7 -hide (open) fact empty_def single_def bind_def union_def if_random_dseq_def not_random_dseq_def Random_def map_def
     1.8 +hide (open) fact empty_def single_def bind_def union_def if_random_dseq_def not_random_dseq_def Random.simps map_def
     1.9  
    1.10  end
    1.11 \ No newline at end of file