diff -r ce9134bdc1d4 -r 2d5b122aa0ff src/HOL/Nonstandard_Analysis/CLim.thy
--- a/src/HOL/Nonstandard_Analysis/CLim.thy	Thu May 02 11:43:56 2019 +0200
+++ b/src/HOL/Nonstandard_Analysis/CLim.thy	Thu May 02 12:58:32 2019 +0100
@@ -100,7 +100,7 @@
 subsection \<open>Continuity\<close>
 
 lemma NSLIM_isContc_iff: "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S f a \<longleftrightarrow> (\<lambda>h. f (a + h)) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S f a"
-  by (rule NSLIM_h_iff)
+  by (rule NSLIM_at0_iff)
 
 
 subsection \<open>Functions from Complex to Reals\<close>