src/HOL/Library/Convex.thy
changeset 59557 ebd8ecacfba6
parent 58881 b9556a055632
child 59862 44b3f4fa33ca
     1.1 --- a/src/HOL/Library/Convex.thy	Wed Feb 18 22:46:48 2015 +0100
     1.2 +++ b/src/HOL/Library/Convex.thy	Thu Feb 19 11:53:36 2015 +0100
     1.3 @@ -329,7 +329,7 @@
     1.4    have "u * f x + v * f y \<le> u * max (f x) (f y) + v * max (f x) (f y)"
     1.5      using assms(4,5) by (auto simp add: mult_left_mono add_mono)
     1.6    also have "\<dots> = max (f x) (f y)"
     1.7 -    using assms(6) unfolding distrib[symmetric] by auto
     1.8 +    using assms(6) by (simp add: distrib_right [symmetric]) 
     1.9    finally show ?thesis
    1.10      using assms unfolding convex_on_def by fastforce
    1.11  qed