[isabelle-dev] NEWS: numeral representation

[Brian Huffman]

On Mon, Mar 26, 2012 at 7:23 PM, Makarius <makarius at sketis.net> wrote:
> On Mon, 26 Mar 2012, Lukas Bulwahn wrote:
>
>> This problem is reproducible on our testboard servers. At the moment, all
>> tests of changesets after 2a1953f0d20d have to be manually aborted because
>> of that reason. I hope you find a solution quickly, otherwise we should
>> deactivate the Proofs-Lambda theory to keep a stable testing environment.
>
>
> OK, I have disabled HOL-Proofs-Lambda for the moment (cf. 500a5d97511a).

This is now fixed in a3a64240cd98, and I have re-enabled HOL-Proofs-Lambda.

The problem was the code equation for function "nat" configured in
Library/Code_Integer.thy which, in conjunction with Int.nat_numeral
[code_abbrev], produced code that looped indefinitely.

- Brian