changeset 31636 | 138625ae4067 |
parent 31633 | ea47e2b63588 |
child 32740 | 9dd0a2f83429 |
--- a/src/HOL/Random.thy Sun Jun 14 17:20:19 2009 +0200 +++ b/src/HOL/Random.thy Mon Jun 15 08:16:08 2009 +0200 @@ -176,7 +176,7 @@ hide (open) type seed hide (open) const inc_shift minus_shift log "next" seed_invariant split_seed - iterate range select pick select_weight select_default + iterate range select pick select_weight no_notation fcomp (infixl "o>" 60) no_notation scomp (infixl "o\<rightarrow>" 60)