[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:

http://www4.in.tum.de/~huffman/cgi-bin/repos.cgi/numerals/rev/350dd336be43
http://www4.in.tum.de/~huffman/cgi-bin/repos.cgi/numerals/rev/df49a9297ced
http://www4.in.tum.de/~huffman/cgi-bin/repos.cgi/numerals/rev/afe641c9b5d8

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