src/HOL/Nonstandard_Analysis/CLim.thy

--- a/src/HOL/Nonstandard_Analysis/CLim.thy	Tue Sep 17 16:21:31 2019 +0100
+++ b/src/HOL/Nonstandard_Analysis/CLim.thy	Wed Sep 18 14:41:37 2019 +0100
@@ -11,7 +11,7 @@
 begin
 
 (*not in simpset?*)
-declare hypreal_epsilon_not_zero [simp]
+declare epsilon_not_zero [simp]
 
 (*??generalize*)
 lemma lemma_complex_mult_inverse_squared [simp]: "x \<noteq> 0 \<Longrightarrow> x * (inverse x)\<^sup>2 = inverse x"