diff -r dd58f13a8eb4 -r eb85850d3eb7 src/HOL/Hyperreal/HLog.thy
--- a/src/HOL/Hyperreal/HLog.thy	Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/Hyperreal/HLog.thy	Fri Nov 17 02:20:03 2006 +0100
@@ -19,10 +19,11 @@
 
 
 definition
-  powhr  :: "[hypreal,hypreal] => hypreal"     (infixr "powhr" 80)
+  powhr  :: "[hypreal,hypreal] => hypreal"     (infixr "powhr" 80) where
   "x powhr a = starfun2 (op powr) x a"
   
-  hlog :: "[hypreal,hypreal] => hypreal"
+definition
+  hlog :: "[hypreal,hypreal] => hypreal" where
   "hlog a x = starfun2 log a x"
 
 declare powhr_def [transfer_unfold]