[isabelle-dev] NEWS: numeral representation

Brian Huffman huffman at in.tum.de
Wed Mar 28 21:59:22 CEST 2012

On Wed, Mar 28, 2012 at 9:15 PM, Florian Haftmann
<florian.haftmann at informatik.tu-muenchen.de> wrote:
> Btw. for the moment you have not transferred by additional changes
> concerning Efficient_Nat etc.  What are your plans for these?  To wait
> until the transition proper has fortified a little?  Or shall I take
> care for these?

Hi Florian,

You had replaced Efficient_Nat.thy with a similar theory file named
Code_Numeral_Nat.thy. I chose to rename this back to Efficient_Nat
before doing the big merge, because it meant touching about a dozen
fewer files, and avoiding breaking lots of AFP entries. I also
reverted the updates that you put in NEWS and the other documentation
related to the rename:


If you still want to use the name "Code_Numeral_Nat", go ahead and put
these changes back in.

Besides the Efficient_Nat/Code_Numeral_Nat naming, is there anything
else that you are still missing?

- Brian

More information about the isabelle-dev mailing list