src/HOL/NSA/NSA.thy

   hnorm :: "'a::real_normed_vector star \<Rightarrow> real star" where
   [transfer_unfold]: "hnorm = *f* norm"
 
 definition
   Infinitesimal  :: "('a::real_normed_vector) star set" where
-  [code del]: "Infinitesimal = {x. \<forall>r \<in> Reals. 0 < r --> hnorm x < r}"
+  "Infinitesimal = {x. \<forall>r \<in> Reals. 0 < r --> hnorm x < r}"
 
 definition
   HFinite :: "('a::real_normed_vector) star set" where
-  [code del]: "HFinite = {x. \<exists>r \<in> Reals. hnorm x < r}"
+  "HFinite = {x. \<exists>r \<in> Reals. hnorm x < r}"
 
 definition
   HInfinite :: "('a::real_normed_vector) star set" where
-  [code del]: "HInfinite = {x. \<forall>r \<in> Reals. r < hnorm x}"
+  "HInfinite = {x. \<forall>r \<in> Reals. r < hnorm x}"
 
 definition
   approx :: "['a::real_normed_vector star, 'a star] => bool"  (infixl "@=" 50) where
     --{*the `infinitely close' relation*}
   "(x @= y) = ((x - y) \<in> Infinitesimal)"

 
 subsection {* Nonstandard Extension of the Norm Function *}
 
 definition
   scaleHR :: "real star \<Rightarrow> 'a star \<Rightarrow> 'a::real_normed_vector star" where
-  [transfer_unfold, code del]: "scaleHR = starfun2 scaleR"
+  [transfer_unfold]: "scaleHR = starfun2 scaleR"
 
 lemma Standard_hnorm [simp]: "x \<in> Standard \<Longrightarrow> hnorm x \<in> Standard"
 by (simp add: hnorm_def)
 
 lemma star_of_norm [simp]: "star_of (norm x) = hnorm (star_of x)"