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