--- a/src/HOL/Nonstandard_Analysis/HDeriv.thy Tue Apr 30 13:01:22 2019 +0100
+++ b/src/HOL/Nonstandard_Analysis/HDeriv.thy Tue Apr 30 14:42:52 2019 +0100
@@ -34,9 +34,6 @@
lemma NS_DERIV_D: "DERIV f x :> D \<Longrightarrow> (\<lambda>h. (f (x + h) - f x) / h) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S D"
by (simp add: DERIV_def LIM_NSLIM_iff)
-lemma hnorm_of_hypreal: "\<And>r. hnorm (( *f* of_real) r::'a::real_normed_div_algebra star) = \<bar>r\<bar>"
- by transfer (rule norm_of_real)
-
lemma Infinitesimal_of_hypreal:
"x \<in> Infinitesimal \<Longrightarrow> (( *f* of_real) x::'a::real_normed_div_algebra star) \<in> Infinitesimal"
by (metis Infinitesimal_of_hypreal_iff of_hypreal_def)