author | berghofe |
Mon, 19 Nov 2001 17:42:00 +0100 | |
changeset 12239 | ee360f910ec8 |
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