--- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Tue Oct 13 09:21:21 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Tue Oct 13 12:42:08 2015 +0100
@@ -1259,7 +1259,7 @@
shows "midpoint x y \<in> convex hull s"
proof -
have "(1 - inverse(2)) *\<^sub>R x + inverse(2) *\<^sub>R y \<in> convex hull s"
- apply (rule mem_convex)
+ apply (rule convexD_alt)
using assms
apply (auto simp: convex_convex_hull)
done
@@ -1649,7 +1649,7 @@
apply (simp add: segment_convex_hull)
apply (rule convex_hull_subset)
using assms
- apply (auto simp: hull_inc c' Convex.mem_convex)
+ apply (auto simp: hull_inc c' Convex.convexD_alt)
done
qed
@@ -1666,7 +1666,7 @@
apply (simp_all add: segment_convex_hull)
apply (rule_tac [!] convex_hull_subset)
using assms
- apply (auto simp: hull_inc c' Convex.mem_convex)
+ apply (auto simp: hull_inc c' Convex.convexD_alt)
done
show ?thesis
apply (rule path_integral_unique)