# HG changeset patch
# User haftmann
# Date 1311539893 -7200
# Node ID 1fe23cfca01f13aa123437d8ba8d330f90997387
# Parent  610efb6bda1fef3957c368145370115e253d17fe
adjusted to tailored version of bex_simps

diff -r 610efb6bda1f -r 1fe23cfca01f src/HOL/Multivariate_Analysis/Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Sun Jul 24 21:27:25 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Sun Jul 24 22:38:13 2011 +0200
@@ -2505,7 +2505,7 @@
       by auto
     from inj_on_image_set_diff[OF "2.prems"(3), of "insert a b " "{a}", symmetric]
     have tha: "f ` insert a b - f ` {a} = f ` (insert a b - {a})" by blast
-    from "2.prems"(2)[unfolded dependent_def bex_simps(10), rule_format, of "f a"]
+    from "2.prems"(2) [unfolded dependent_def bex_simps(8), rule_format, of "f a"]
     have "f a \<notin> span (f ` b)" using tha
       using "2.hyps"(2)
       "2.prems"(3) by auto