[isabelle-dev] NEWS: powr
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