src/HOL/NSA/HyperDef.thy

 done
 *)
 
 subsection{*Powers with Hypernatural Exponents*}
 
-definition pow :: "['a::recpower star, nat star] \<Rightarrow> 'a star" (infixr "pow" 80) where
+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"
   (* hypernatural powers of hyperreals *)
 
 lemma Standard_hyperpow [simp]:
   "\<lbrakk>r \<in> Standard; n \<in> Standard\<rbrakk> \<Longrightarrow> r pow n \<in> Standard"

 lemma hyperpow_add:
   "\<And>r n m. (r::'a::recpower star) pow (n + m) = (r pow n) * (r pow m)"
 by transfer (rule power_add)
 
 lemma hyperpow_one [simp]:
-  "\<And>r. (r::'a::recpower star) pow (1::hypnat) = r"
+  "\<And>r. (r::'a::monoid_mult star) pow (1::hypnat) = r"
 by transfer (rule power_one_right)
 
 lemma hyperpow_two:
   "\<And>r. (r::'a::recpower star) pow ((1::hypnat) + (1::hypnat)) = r * r"
 by transfer (simp add: power_Suc)