--- a/src/HOL/Nonstandard_Analysis/HLim.thy Tue Oct 10 14:03:51 2017 +0100
+++ b/src/HOL/Nonstandard_Analysis/HLim.thy Tue Oct 10 17:15:37 2017 +0100
@@ -234,7 +234,7 @@
lemma isNSCont_inverse: "isNSCont f x \<Longrightarrow> f x \<noteq> 0 \<Longrightarrow> isNSCont (\<lambda>x. inverse (f x)) x"
for f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_div_algebra"
- by (auto intro: isCont_inverse simp add: isNSCont_isCont_iff)
+ by (auto intro: continuous_at_inverse simp add: isNSCont_isCont_iff)
lemma isNSCont_const [simp]: "isNSCont (\<lambda>x. k) a"
by (simp add: isNSCont_def)