[isabelle-dev] NEWS: powr

[Larry Paulson]

All I know is that HOL-Codegenerator_Test failed because of some (?) type-related ambiguity connected with powr, with no indication of where this instance of powr actually was. Adding [code del] to its definition eliminated the error, God knows why.

Larry

> On 12 Apr 2015, at 20:03, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de> wrote:
> 
> 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.