[isabelle-dev] NEWS: numeral representation

[Makarius]

On Sun, 25 Mar 2012, Brian Huffman wrote:

> As of 2a1953f0d20d, Isabelle now has a new representation for binary 
> numerals

Execellent, this is a big step forward in this important reform.  It seems 
we now have the main parts in place, so that we can start consolidating 
towards the release over a couple of weeks.  (I am still unsure myself, 
when the release point will be precisely.)


Another pending issue of 2a1953f0d20d is HOL-Proofs-Lambda.  When run in 
parallel it fills up > 25 GB of memory on my 32 GB machine.  When run in 
x86 mode, it runs out of stack on polyml-5.4.1.  The critical spot might 
be a definition of datatype or datatype realizer.

This needs further investigation.  Do you have any ideas on the spot?


 	Makarius