where there is nothing, nothing can be hidden
authorhaftmann
Mon Jun 15 08:16:08 2009 +0200 (2009-06-15)
changeset 31636138625ae4067
parent 31635 8623244a50d5
child 31637 e1223f58ea9b
where there is nothing, nothing can be hidden
src/HOL/Random.thy
     1.1 --- a/src/HOL/Random.thy	Sun Jun 14 17:20:19 2009 +0200
     1.2 +++ b/src/HOL/Random.thy	Mon Jun 15 08:16:08 2009 +0200
     1.3 @@ -176,7 +176,7 @@
     1.4  
     1.5  hide (open) type seed
     1.6  hide (open) const inc_shift minus_shift log "next" seed_invariant split_seed
     1.7 -  iterate range select pick select_weight select_default
     1.8 +  iterate range select pick select_weight
     1.9  
    1.10  no_notation fcomp (infixl "o>" 60)
    1.11  no_notation scomp (infixl "o\<rightarrow>" 60)