equal
deleted
inserted
replaced
12 powr :: "[real,real] => real" (infixr "powr" 80) |
12 powr :: "[real,real] => real" (infixr "powr" 80) |
13 --{*exponentation with real exponent*} |
13 --{*exponentation with real exponent*} |
14 "x powr a == exp(a * ln x)" |
14 "x powr a == exp(a * ln x)" |
15 |
15 |
16 log :: "[real,real] => real" |
16 log :: "[real,real] => real" |
17 --{*logarithm of @[term x} to base @[term a}*} |
17 --{*logarithm of @{term x} to base @{term a}*} |
18 "log a x == ln x / ln a" |
18 "log a x == ln x / ln a" |
19 |
19 |
20 |
20 |
21 |
21 |
22 lemma powr_one_eq_one [simp]: "1 powr a = 1" |
22 lemma powr_one_eq_one [simp]: "1 powr a = 1" |