src/HOL/Hyperreal/HyperNat.thy

   hypnat_of_nat :: "nat => nat star" where
   "hypnat_of_nat == star_of"
 
 definition
   hSuc :: "hypnat => hypnat" where
-  hSuc_def [transfer_unfold]: "hSuc = *f* Suc"
+  hSuc_def [transfer_unfold, code func del]: "hSuc = *f* Suc"
 
 subsection{*Properties Transferred from Naturals*}
 
 lemma hSuc_not_zero [iff]: "\<And>m. hSuc m \<noteq> 0"
 by transfer (rule Suc_not_Zero)

 
 subsection {* Embedding of the Hypernaturals into other types *}
 
 definition
   of_hypnat :: "hypnat \<Rightarrow> 'a::semiring_1_cancel star" where
-  of_hypnat_def [transfer_unfold]: "of_hypnat = *f* of_nat"
+  of_hypnat_def [transfer_unfold, code func del]: "of_hypnat = *f* of_nat"
 
 lemma of_hypnat_0 [simp]: "of_hypnat 0 = 0"
 by transfer (rule of_nat_0)
 
 lemma of_hypnat_1 [simp]: "of_hypnat 1 = 1"