--- a/src/HOL/NSA/HyperDef.thy Mon Apr 27 08:22:37 2009 +0200
+++ b/src/HOL/NSA/HyperDef.thy Mon Apr 27 10:11:44 2009 +0200
@@ -426,7 +426,7 @@
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 *)
@@ -459,7 +459,7 @@
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: