[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