| changeset 30968 | 10fef94f40fc |
| parent 30273 | ecd6f0ca62ea |
| child 31001 | 7e6ffd8f51a9 |
--- a/src/HOL/NSA/HyperDef.thy Thu Apr 23 12:17:51 2009 +0200 +++ b/src/HOL/NSA/HyperDef.thy Thu Apr 23 12:17:51 2009 +0200 @@ -426,7 +426,7 @@ subsection{*Powers with Hypernatural Exponents*} -definition pow :: "['a::power star, nat star] \<Rightarrow> 'a star" (infixr "pow" 80) where +definition pow :: "['a::recpower 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 *)