| author | paulson |
| Thu, 18 Dec 2003 15:06:24 +0100 | |
| changeset 14301 | 48dc606749bd |
| parent 13958 | c1c67582c9b5 |
| child 14411 | 7851e526b8b7 |
| permissions | -rw-r--r-- |
| 13958 | 1 |
(* Title : HLog.thy |
2 |
Author : Jacques D. Fleuriot |
|
3 |
Copyright : 2000,2001 University of Edinburgh |
|
4 |
Description : hyperreal base logarithms |
|
5 |
*) |
|
6 |
||
7 |
HLog = Log + HTranscendental + |
|
8 |
||
9 |
||
10 |
constdefs |
|
11 |
||
12 |
powhr :: [hypreal,hypreal] => hypreal (infixr 80) |
|
13 |
"x powhr a == ( *f* exp) (a * ( *f* ln) x)" |
|
14 |
||
15 |
hlog :: [hypreal,hypreal] => hypreal |
|
16 |
"hlog a x == Abs_hypreal(UN A: Rep_hypreal(a).UN X: Rep_hypreal(x). |
|
17 |
hyprel `` {%n. log (A n) (X n)})"
|
|
18 |
||
19 |
end |