equal
deleted
inserted
replaced
9 theory Log |
9 theory Log |
10 imports Transcendental |
10 imports Transcendental |
11 begin |
11 begin |
12 |
12 |
13 definition |
13 definition |
14 powr :: "[real,real] => real" (infixr "powr" 80) |
14 powr :: "[real,real] => real" (infixr "powr" 80) where |
15 --{*exponentation with real exponent*} |
15 --{*exponentation with real exponent*} |
16 "x powr a = exp(a * ln x)" |
16 "x powr a = exp(a * ln x)" |
17 |
17 |
18 log :: "[real,real] => real" |
18 definition |
|
19 log :: "[real,real] => real" where |
19 --{*logarithm of @{term x} to base @{term a}*} |
20 --{*logarithm of @{term x} to base @{term a}*} |
20 "log a x = ln x / ln a" |
21 "log a x = ln x / ln a" |
21 |
22 |
22 |
23 |
23 |
24 |