| changeset 60020 | 065ecea354d0 |
| parent 60017 | b785d6d06430 |
| child 60035 | 4b77fc0b3514 |
--- a/src/HOL/Transcendental.thy Sat Apr 11 16:19:59 2015 +0100 +++ b/src/HOL/Transcendental.thy Sat Apr 11 22:18:33 2015 +0100 @@ -1291,7 +1291,7 @@ definition powr :: "['a,'a] => 'a::ln" (infixr "powr" 80) -- {*exponentation via ln and exp*} - where "x powr a \<equiv> if x = 0 then 0 else exp(a * ln x)" + where [code del]: "x powr a \<equiv> if x = 0 then 0 else exp(a * ln x)" instantiation real :: ln