author | kleing |
Tue, 13 May 2003 08:59:21 +0200 | |
changeset 14024 | 213dcc39358f |
parent 12224 | 02df7cbe7d25 |
child 14411 | 7851e526b8b7 |
permissions | -rw-r--r-- |
(* 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