src/HOL/NSA/HyperDef.thy

 
 instantiation star :: (scaleR) scaleR
 begin
 
 definition
-  star_scaleR_def [transfer_unfold, code del]: "scaleR r \<equiv> *f* (scaleR r)"
+  star_scaleR_def [transfer_unfold]: "scaleR r \<equiv> *f* (scaleR r)"
 
 instance ..
 
 end
 

 
 subsection {* Injection from @{typ hypreal} *}
 
 definition
   of_hypreal :: "hypreal \<Rightarrow> 'a::real_algebra_1 star" where
-  [transfer_unfold, code del]: "of_hypreal = *f* of_real"
+  [transfer_unfold]: "of_hypreal = *f* of_real"
 
 lemma Standard_of_hypreal [simp]:
   "r \<in> Standard \<Longrightarrow> of_hypreal r \<in> Standard"
 by (simp add: of_hypreal_def)
 

 *)
 
 subsection{*Powers with Hypernatural Exponents*}
 
 definition pow :: "['a::power star, nat star] \<Rightarrow> 'a star" (infixr "pow" 80) where
-  hyperpow_def [transfer_unfold, code del]: "R pow N = ( *f2* op ^) R N"
+  hyperpow_def [transfer_unfold]: "R pow N = ( *f2* op ^) R N"
   (* hypernatural powers of hyperreals *)
 
 lemma Standard_hyperpow [simp]:
   "\<lbrakk>r \<in> Standard; n \<in> Standard\<rbrakk> \<Longrightarrow> r pow n \<in> Standard"
 unfolding hyperpow_def by simp