--- a/src/HOL/NSA/HLog.thy Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/NSA/HLog.thy Fri Oct 10 06:45:53 2008 +0200
@@ -20,11 +20,11 @@
definition
powhr :: "[hypreal,hypreal] => hypreal" (infixr "powhr" 80) where
- [transfer_unfold, code func del]: "x powhr a = starfun2 (op powr) x a"
+ [transfer_unfold, code del]: "x powhr a = starfun2 (op powr) x a"
definition
hlog :: "[hypreal,hypreal] => hypreal" where
- [transfer_unfold, code func del]: "hlog a x = starfun2 log a x"
+ [transfer_unfold, code del]: "hlog a x = starfun2 log a x"
lemma powhr: "(star_n X) powhr (star_n Y) = star_n (%n. (X n) powr (Y n))"
by (simp add: powhr_def starfun2_star_n)