src/HOL/Nonstandard_Analysis/HDeriv.thy

 lemma NSDERIV_cmult_Id [simp]: "NSDERIV ((*) c) x :> c"
   using NSDERIV_Id [THEN NSDERIV_cmult] by simp
 
 lemma NSDERIV_inverse:
   fixes x :: "'a::real_normed_field"
-  assumes "x \<noteq> 0" \<comment> \<open>can't get rid of @{term "x \<noteq> 0"} because it isn't continuous at zero\<close>
+  assumes "x \<noteq> 0" \<comment> \<open>can't get rid of \<^term>\<open>x \<noteq> 0\<close> because it isn't continuous at zero\<close>
   shows "NSDERIV (\<lambda>x. inverse x) x :> - (inverse x ^ Suc (Suc 0))"
 proof -
   {
     fix h :: "'a star"
     assume h_Inf: "h \<in> Infinitesimal"