src/HOL/Random_Sequence.thy
changeset 34953 a053ad2a7a72
parent 34948 2d5f2a9f7601
child 36176 3fe7e97ccca8
equal deleted inserted replaced
34952:bd7e347eb768 34953:a053ad2a7a72
    54 *)
    54 *)
    55 
    55 
    56 hide (open) const empty single bind union if_random_dseq not_random_dseq Random map
    56 hide (open) const empty single bind union if_random_dseq not_random_dseq Random map
    57 
    57 
    58 hide type DSequence.dseq random_dseq
    58 hide type DSequence.dseq random_dseq
    59 hide (open) fact empty_def single_def bind_def union_def if_random_dseq_def not_random_dseq_def Random_def map_def
    59 hide (open) fact empty_def single_def bind_def union_def if_random_dseq_def not_random_dseq_def Random.simps map_def
    60 
    60 
    61 end
    61 end