[isabelle-dev] NEWS: powr

[Larry Paulson]

You should always have success by unfolding powr_def. And I’m told that the necessary changes to “approximation” are not difficult.

Larry

> 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.
> 
> 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