# HG changeset patch
# User wenzelm
# Date 1358531212 -3600
# Node ID 9efd58e1e07cc129c047b1913bf308a905d4d521
# Parent  73ec6ad6700ec00d7c7e29d074b1666bbbe31b3f
tuned proof -- much faster;

diff -r 73ec6ad6700e -r 9efd58e1e07c src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri Jan 18 17:51:50 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri Jan 18 18:46:52 2013 +0100
@@ -5445,7 +5445,7 @@
 have *: "S Int closure T = S" using assms by auto
 have "~(rel_interior S <= rel_frontier T)"
      using closure_mono[of "rel_interior S" "rel_frontier T"] closed_rel_frontier[of T]
-     closure_closed convex_closure_rel_interior[of S] closure_subset[of S] assms by auto
+     closure_closed[of S] convex_closure_rel_interior[of S] closure_subset[of S] assms by auto
 hence "(rel_interior S) Int (rel_interior (closure T)) ~= {}"
      using assms rel_frontier_def[of T] rel_interior_subset convex_rel_interior_closure[of T] by auto
 hence "rel_interior S Int rel_interior T = rel_interior (S Int closure T)" using assms convex_closure