Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Analysis/Further_Topology.thy
changeset 70532 fcf3b891ccb1
parent 70196 b7ef9090feed
child 70620 f95193669ad7 
--- a/src/HOL/Analysis/Further_Topology.thy	Wed Aug 14 19:50:23 2019 +0200
+++ b/src/HOL/Analysis/Further_Topology.thy	Thu Aug 15 16:11:56 2019 +0100
@@ -4020,7 +4020,7 @@
       apply (auto simp: exp_eq dist_norm norm_mult)
       done
     then have "((\<lambda>y. (g y - g z) / (y - z)) \<longlongrightarrow> f' / exp (g z)) (at z within S)"
-      by (auto intro!: Lim_transform_eventually [OF _ tendsto_divide [OF ee dd]])
+      by (auto intro!: Lim_transform_eventually [OF tendsto_divide [OF ee dd]])
     then show ?thesis
       by (auto simp: field_differentiable_def has_field_derivative_iff)
   qed
@@ -4068,7 +4068,7 @@
       apply (auto simp: exp_eq dist_norm norm_mult)
       done
     then have "((\<lambda>y. (g y - g z) / (y - z)) \<longlongrightarrow> f' / exp (g z)) (at z within S)"
-      by (auto intro!: Lim_transform_eventually [OF _ tendsto_divide [OF ee dd]])
+      by (auto intro!: Lim_transform_eventually [OF tendsto_divide [OF ee dd]])
     then show ?thesis
       by (auto simp: field_differentiable_def has_field_derivative_iff)
   qed
isabelle