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