src/HOL/Library/Convex.thy

   assumes "\<And>t x y. t > 0 \<Longrightarrow> t < 1 \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x < y \<Longrightarrow>
              f ((1 - t) *\<^sub>R x + t *\<^sub>R y) \<le> (1 - t) * f x + t * f y"
   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:
   assumes "convex_on A f"
   shows   "\<And>t x y. t \<ge> 0 \<Longrightarrow> t \<le> 1 \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow>