[isabelle-dev] NEWS: powr
florian.haftmann at informatik.tu-muenchen.de
Sun Apr 12 21:03:38 CEST 2015
>> * 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.
from inspecting your diffs
hg diff -c b785d6d06430 | grep code
hg diff -c 065ecea354d0 | grep code
I see that both hardly tinker with code declarations anyway.
And previously the definitions of ln and powr have been the same on real
as they are now. So, there should hardly have been any working code
setup before, and I can confirm that there is no such setup in Isabelle2014.
Maybe there has been some particular support in the approximation
method, but I do not know the details of that.
Hope this helps,
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 198 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev