[isabelle-dev] NEWS: powr

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Sun Apr 12 21:03:38 CEST 2015


Hi Larry,

>> * 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,
	Florian

> 
> Larry
> 
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 198 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20150412/01ffea85/attachment.sig>


More information about the isabelle-dev mailing list