src/HOL/Random.thy
changeset 31196 82ff416d7d66
parent 31186 b458b4ac570f
child 31203 5c8fb4fd67e0
--- 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\<rightarrow>" 60)