changeset 36176 | 3fe7e97ccca8 |
parent 36020 | 3ee4c29ead7f |
child 36538 | 4fe16d49283b |
--- a/src/HOL/Random.thy Fri Apr 16 20:56:40 2010 +0200 +++ b/src/HOL/Random.thy Fri Apr 16 21:28:09 2010 +0200 @@ -174,10 +174,10 @@ end; *} -hide (open) type seed -hide (open) const inc_shift minus_shift log "next" split_seed +hide_type (open) seed +hide_const (open) inc_shift minus_shift log "next" split_seed iterate range select pick select_weight -hide (open) fact range_def +hide_fact (open) range_def no_notation fcomp (infixl "o>" 60) no_notation scomp (infixl "o\<rightarrow>" 60)