# HG changeset patch # User haftmann # Date 1242654342 -7200 # Node ID 82ff416d7d6628fcdbb806f43994ce6dce6af437 # Parent 12741f23527dfb43e2a8d37d0dd03431489165d2 hide fact log_def -- should not shadow regular log definition diff -r 12741f23527d -r 82ff416d7d66 src/HOL/Random.thy --- a/src/HOL/Random.thy Mon May 18 15:45:42 2009 +0200 +++ b/src/HOL/Random.thy Mon May 18 15:45:42 2009 +0200 @@ -169,6 +169,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 +hide (open) fact log_def no_notation fcomp (infixl "o>" 60) no_notation scomp (infixl "o\" 60)