[isabelle-dev] NEWS: powr

[Manuel Eberl]

I am not terribly happy about that. I use approximation of powr in my work on Akra–Bazzi and the Master theorem.

I take it that a powr b = exp (ln a * b) still holds for positive a. I could probably apply that rewrite rule before applying approximation, but it would of course be nice if I did not have to.

The issue is, however, not terribly urgent since my project is still several weeks from being finished, and I only need approximation for a small part that is independent from everything else.

Manuel

 Larry Paulson <lp15 at cam.ac.uk> wrote:

>> * Complex powers and square roots. The functions "ln" and "powr" are now
>> overloaded for types real and complex, and 0 powr y = 0 by definition.
>> INCOMPATIBILITY: type constraints may be necessary.
>
>But I had to remove support for powr in code generation and the approximation method. If anybody thinks these are priorities for restoration, I guess we only have a few days. The problem with code generation has something to do with types.
>
>Larry
>
>
>_______________________________________________
>isabelle-dev mailing list
>isabelle-dev at in.tum.de
>https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev