1.1 --- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Sun Jul 24 21:27:25 2011 +0200
1.2 +++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Sun Jul 24 22:38:13 2011 +0200
1.3 @@ -2505,7 +2505,7 @@
1.4 by auto
1.5 from inj_on_image_set_diff[OF "2.prems"(3), of "insert a b " "{a}", symmetric]
1.6 have tha: "f ` insert a b - f ` {a} = f ` (insert a b - {a})" by blast
1.7 - from "2.prems"(2)[unfolded dependent_def bex_simps(10), rule_format, of "f a"]
1.8 + from "2.prems"(2) [unfolded dependent_def bex_simps(8), rule_format, of "f a"]
1.9 have "f a \<notin> span (f ` b)" using tha
1.10 using "2.hyps"(2)
1.11 "2.prems"(3) by auto