hide fact range_def
authorhaftmann
Fri Feb 19 14:47:00 2010 +0100 (2010-02-19)
changeset 3526607a56610c00b
parent 35265 3fd8c3edf639
child 35267 8dfd816713c6
hide fact range_def
src/HOL/Random.thy
     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)