src/HOL/Hyperreal/Log.thy

--- a/src/HOL/Hyperreal/Log.thy	Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/Hyperreal/Log.thy	Fri Nov 17 02:20:03 2006 +0100
@@ -11,11 +11,12 @@
 begin
 
 definition
-  powr  :: "[real,real] => real"     (infixr "powr" 80)
+  powr  :: "[real,real] => real"     (infixr "powr" 80) where
     --{*exponentation with real exponent*}
   "x powr a = exp(a * ln x)"
 
-  log :: "[real,real] => real"
+definition
+  log :: "[real,real] => real" where
     --{*logarithm of @{term x} to base @{term a}*}
   "log a x = ln x / ln a"