[isabelle-dev] NEWS: powr
lp15 at cam.ac.uk
Sun Apr 12 17:38:13 CEST 2015
You should always have success by unfolding powr_def. And I’m told that the necessary changes to “approximation” are not difficult.
> On 12 Apr 2015, at 12:26, Manuel Eberl <eberlm at in.tum.de> wrote:
> 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