[isabelle-dev] NEWS: powr

Larry Paulson lp15 at cam.ac.uk
Sun Apr 12 23:16:23 CEST 2015

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.


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

More information about the isabelle-dev mailing list