src/HOL/Library/Convex.thy

--- a/src/HOL/Library/Convex.thy	Tue Mar 31 00:21:07 2015 +0200
+++ b/src/HOL/Library/Convex.thy	Tue Mar 31 15:00:03 2015 +0100
@@ -121,6 +121,9 @@
   then show "convex {a<..<b}" by (simp only: convex_Int 3 4)
 qed
 
+lemma convex_Reals: "convex Reals"
+  by (simp add: convex_def scaleR_conv_of_real)
+    
 subsection {* Explicit expressions for convexity in terms of arbitrary sums. *}
 
 lemma convex_setsum: