src/HOL/Probability/Information.thy
changeset 41413 64cd30d6b0b8
parent 41095 c335d880ff82
child 41661 baf1964bc468
     1.1 --- a/src/HOL/Probability/Information.thy	Wed Dec 29 13:51:17 2010 +0100
     1.2 +++ b/src/HOL/Probability/Information.thy	Wed Dec 29 17:34:41 2010 +0100
     1.3 @@ -1,5 +1,8 @@
     1.4  theory Information
     1.5 -imports Probability_Space Convex Lebesgue_Measure
     1.6 +imports
     1.7 +  Probability_Space
     1.8 +  "~~/src/HOL/Library/Convex"
     1.9 +  Lebesgue_Measure
    1.10  begin
    1.11  
    1.12  lemma log_le: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> x \<le> y \<Longrightarrow> log a x \<le> log a y"