src/HOL/Random.thy
changeset 31196 82ff416d7d66
parent 31186 b458b4ac570f
child 31203 5c8fb4fd67e0
equal deleted inserted replaced
31195:12741f23527d 31196:82ff416d7d66
   167 *}
   167 *}
   168 
   168 
   169 hide (open) type seed
   169 hide (open) type seed
   170 hide (open) const inc_shift minus_shift log "next" seed_invariant split_seed
   170 hide (open) const inc_shift minus_shift log "next" seed_invariant split_seed
   171   iterate range select pick select_weight select_default
   171   iterate range select pick select_weight select_default
       
   172 hide (open) fact log_def
   172 
   173 
   173 no_notation fcomp (infixl "o>" 60)
   174 no_notation fcomp (infixl "o>" 60)
   174 no_notation scomp (infixl "o\<rightarrow>" 60)
   175 no_notation scomp (infixl "o\<rightarrow>" 60)
   175 
   176 
   176 end
   177 end