src/HOL/Multivariate_Analysis/Derivative.thy
changeset 62101 26c0a70f78a3
parent 62087 44841d07ef1d
child 62207 45eee631ea4f
     1.1 --- a/src/HOL/Multivariate_Analysis/Derivative.thy	Fri Jan 08 16:37:56 2016 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Fri Jan 08 17:40:59 2016 +0100
     1.3 @@ -874,8 +874,7 @@
     1.4            unfolding eventually_at_topological
     1.5            by metis
     1.6          from \<open>open S\<close> obtain d where d: "\<And>x. dist x y < d \<Longrightarrow> x \<in> S" "d > 0"
     1.7 -          by (force simp: dist_commute open_real_def ball_def
     1.8 -            dest!: bspec[OF _ \<open>y \<in> S\<close>])
     1.9 +          by (force simp: dist_commute open_dist ball_def dest!: bspec[OF _ \<open>y \<in> S\<close>])
    1.10          def d' \<equiv> "min ((y + b)/2) (y + (d/2))"
    1.11          have "d' \<in> A"
    1.12            unfolding A_def
    1.13 @@ -939,8 +938,7 @@
    1.14        where S: "open S" "y \<in> S" "\<And>x. x\<in>S \<Longrightarrow> x \<in> {y..b} \<Longrightarrow> ?le x"
    1.15          by metis
    1.16        from \<open>open S\<close> obtain d where d: "\<And>x. dist x y < d \<Longrightarrow> x \<in> S" "d > 0"
    1.17 -        by (force simp: dist_commute open_real_def ball_def
    1.18 -          dest!: bspec[OF _ \<open>y \<in> S\<close>])
    1.19 +        by (force simp: dist_commute open_dist ball_def dest!: bspec[OF _ \<open>y \<in> S\<close>])
    1.20        def d' \<equiv> "min b (y + (d/2))"
    1.21        have "d' \<in> A"
    1.22          unfolding A_def