src/HOL/Random.thy
changeset 35266 07a56610c00b
parent 33236 ea75c6ea643e
child 36020 3ee4c29ead7f
     1.1 --- a/src/HOL/Random.thy	Fri Feb 19 14:47:00 2010 +0100
     1.2 +++ b/src/HOL/Random.thy	Fri Feb 19 14:47:00 2010 +0100
     1.3 @@ -168,6 +168,7 @@
     1.4  hide (open) type seed
     1.5  hide (open) const inc_shift minus_shift log "next" split_seed
     1.6    iterate range select pick select_weight
     1.7 +hide (open) fact range_def
     1.8  
     1.9  no_notation fcomp (infixl "o>" 60)
    1.10  no_notation scomp (infixl "o\<rightarrow>" 60)