[isabelle-dev] NEWS: powr

Manuel Eberl eberlm at in.tum.de
Sun Apr 12 13:26:52 CEST 2015

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.


 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.
>isabelle-dev mailing list
>isabelle-dev at in.tum.de

More information about the isabelle-dev mailing list