src/HOL/Probability/Information.thy

--- a/src/HOL/Probability/Information.thy	Sun Aug 07 12:10:49 2016 +0200
+++ b/src/HOL/Probability/Information.thy	Fri Aug 05 18:34:57 2016 +0200
@@ -8,7 +8,6 @@
 theory Information
 imports
   Independent_Family
-  "~~/src/HOL/Library/Convex"
 begin
 
 lemma log_le: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> x \<le> y \<Longrightarrow> log a x \<le> log a y"