src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
changeset 59815 cce82e360c2f
parent 59765 26d1c71784f1
child 60017 b785d6d06430
     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Mar 23 19:05:14 2015 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Mar 23 19:05:14 2015 +0100
     1.3 @@ -5392,11 +5392,7 @@
     1.4      unfolding mem_interior by auto
     1.5    then have "ball (x - a) e \<subseteq> s"
     1.6      unfolding subset_eq Ball_def mem_ball dist_norm
     1.7 -    apply auto
     1.8 -    apply (erule_tac x="a + xa" in allE)
     1.9 -    unfolding ab_group_add_class.diff_diff_eq[symmetric]
    1.10 -    apply auto
    1.11 -    done
    1.12 +    by (auto simp add: diff_diff_eq)
    1.13    then show "x \<in> op + a ` interior s"
    1.14      unfolding image_iff
    1.15      apply (rule_tac x="x - a" in bexI)