1.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Fri Jan 18 17:51:50 2013 +0100
1.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Fri Jan 18 18:46:52 2013 +0100
1.3 @@ -5445,7 +5445,7 @@
1.4 have *: "S Int closure T = S" using assms by auto
1.5 have "~(rel_interior S <= rel_frontier T)"
1.6 using closure_mono[of "rel_interior S" "rel_frontier T"] closed_rel_frontier[of T]
1.7 - closure_closed convex_closure_rel_interior[of S] closure_subset[of S] assms by auto
1.8 + closure_closed[of S] convex_closure_rel_interior[of S] closure_subset[of S] assms by auto
1.9 hence "(rel_interior S) Int (rel_interior (closure T)) ~= {}"
1.10 using assms rel_frontier_def[of T] rel_interior_subset convex_rel_interior_closure[of T] by auto
1.11 hence "rel_interior S Int rel_interior T = rel_interior (S Int closure T)" using assms convex_closure