hide fact log_def -- should not shadow regular log definition
authorhaftmann
Mon May 18 15:45:42 2009 +0200 (2009-05-18)
changeset 3119682ff416d7d66
parent 31195 12741f23527d
child 31198 ed955d2fbfa9
child 31202 52d332f8f909
hide fact log_def -- should not shadow regular log definition
src/HOL/Random.thy
     1.1 --- a/src/HOL/Random.thy	Mon May 18 15:45:42 2009 +0200
     1.2 +++ b/src/HOL/Random.thy	Mon May 18 15:45:42 2009 +0200
     1.3 @@ -169,6 +169,7 @@
     1.4  hide (open) type seed
     1.5  hide (open) const inc_shift minus_shift log "next" seed_invariant split_seed
     1.6    iterate range select pick select_weight select_default
     1.7 +hide (open) fact log_def
     1.8  
     1.9  no_notation fcomp (infixl "o>" 60)
    1.10  no_notation scomp (infixl "o\<rightarrow>" 60)