# HG changeset patch
# User wenzelm
# Date 1456428905 -3600
# Node ID f1b0908028cfed1a6f5967e6fff2d0a806b64302
# Parent  d515293f59709f342907224417f0055af17ade58
tuned proof;

diff -r d515293f5970 -r f1b0908028cf src/HOL/Library/Convex.thy
--- a/src/HOL/Library/Convex.thy	Thu Feb 25 20:23:32 2016 +0100
+++ b/src/HOL/Library/Convex.thy	Thu Feb 25 20:35:05 2016 +0100
@@ -323,9 +323,9 @@
   shows   "convex_on A f"
 proof
   fix t x y assume A: "x \<in> A" "y \<in> A" "(t::real) > 0" "t < 1"
-  case (goal1 t x y)
-  with goal1 assms[of t x y] assms[of "1 - t" y x]
-    show ?case by (cases x y rule: linorder_cases) (auto simp: algebra_simps)
+  with assms[of t x y] assms[of "1 - t" y x]
+  show "f ((1 - t) *\<^sub>R x + t *\<^sub>R y) \<le> (1 - t) * f x + t * f y"
+    by (cases x y rule: linorder_cases) (auto simp: algebra_simps)
 qed
 
 lemma convex_onD: