src/HOL/Random_Sequence.thy
changeset 36176 3fe7e97ccca8
parent 34953 a053ad2a7a72
child 42163 392fd6c4669c
     1.1 --- a/src/HOL/Random_Sequence.thy	Fri Apr 16 20:56:40 2010 +0200
     1.2 +++ b/src/HOL/Random_Sequence.thy	Fri Apr 16 21:28:09 2010 +0200
     1.3 @@ -48,14 +48,14 @@
     1.4    "map f P = bind P (single o f)"
     1.5  
     1.6  (*
     1.7 -hide const DSequence.empty DSequence.single DSequence.eval
     1.8 +hide_const DSequence.empty DSequence.single DSequence.eval
     1.9    DSequence.map_seq DSequence.bind DSequence.union DSequence.if_seq DSequence.not_seq
    1.10    DSequence.map
    1.11  *)
    1.12  
    1.13 -hide (open) const empty single bind union if_random_dseq not_random_dseq Random map
    1.14 +hide_const (open) empty single bind union if_random_dseq not_random_dseq Random map
    1.15  
    1.16 -hide type DSequence.dseq random_dseq
    1.17 -hide (open) fact empty_def single_def bind_def union_def if_random_dseq_def not_random_dseq_def Random.simps map_def
    1.18 +hide_type DSequence.dseq random_dseq
    1.19 +hide_fact (open) empty_def single_def bind_def union_def if_random_dseq_def not_random_dseq_def Random.simps map_def
    1.20  
    1.21  end
    1.22 \ No newline at end of file