src/HOL/Probability/Information.thy
changeset 60017 b785d6d06430
parent 58876 1888e3cb8048
child 60580 7e741e22d7fc
     1.1 --- a/src/HOL/Probability/Information.thy	Thu Apr 09 20:42:38 2015 +0200
     1.2 +++ b/src/HOL/Probability/Information.thy	Sat Apr 11 11:56:40 2015 +0100
     1.3 @@ -46,7 +46,7 @@
     1.4      finally have "exp u \<noteq> x"
     1.5        by auto }
     1.6    then show "log b x = log b 0"
     1.7 -    by (simp add: log_def ln_def)
     1.8 +    by (simp add: log_def ln_real_def)
     1.9  qed
    1.10  
    1.11  lemma log_mult_eq: