src/HOL/Hyperreal/Log.thy
author paulson
Fri Nov 16 18:24:11 2001 +0100 (2001-11-16)
changeset 12224 02df7cbe7d25
child 14411 7851e526b8b7
permissions -rw-r--r--
even more theories from Jacques
paulson@12224
     1
(*  Title       : Log.thy
paulson@12224
     2
    Author      : Jacques D. Fleuriot
paulson@12224
     3
    Copyright   : 2000,2001 University of Edinburgh
paulson@12224
     4
    Description : standard logarithms only 
paulson@12224
     5
*)
paulson@12224
     6
paulson@12224
     7
Log = Transcendental +
paulson@12224
     8
paulson@12224
     9
constdefs
paulson@12224
    10
paulson@12224
    11
    (* power function with exponent a *)
paulson@12224
    12
    powr  :: [real,real] => real     (infixr 80)
paulson@12224
    13
    "x powr a == exp(a * ln x)"
paulson@12224
    14
paulson@12224
    15
    (* logarithm of x to base a *)
paulson@12224
    16
    log :: [real,real] => real
paulson@12224
    17
    "log a x == ln x / ln a"
paulson@12224
    18
paulson@12224
    19
end