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