diff -r d5e76c2e335c -r 02df7cbe7d25 src/HOL/Hyperreal/Log.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Hyperreal/Log.thy	Fri Nov 16 18:24:11 2001 +0100
@@ -0,0 +1,19 @@
+(*  Title       : Log.thy
+    Author      : Jacques D. Fleuriot
+    Copyright   : 2000,2001 University of Edinburgh
+    Description : standard logarithms only 
+*)
+
+Log = Transcendental +
+
+constdefs
+
+    (* power function with exponent a *)
+    powr  :: [real,real] => real     (infixr 80)
+    "x powr a == exp(a * ln x)"
+
+    (* logarithm of x to base a *)
+    log :: [real,real] => real
+    "log a x == ln x / ln a"
+
+end