src/HOL/Library/Convex.thy
changeset 61070 b72a990adfe2
parent 60449 229bad93377e
child 61426 d53db136e8fd
     1.1 --- a/src/HOL/Library/Convex.thy	Mon Aug 31 21:01:21 2015 +0200
     1.2 +++ b/src/HOL/Library/Convex.thy	Mon Aug 31 21:28:08 2015 +0200
     1.3 @@ -137,7 +137,7 @@
     1.4      by (simp only: convex_Int 3 4)
     1.5  qed
     1.6  
     1.7 -lemma convex_Reals: "convex Reals"
     1.8 +lemma convex_Reals: "convex \<real>"
     1.9    by (simp add: convex_def scaleR_conv_of_real)
    1.10  
    1.11