[isabelle-dev] NEWS: numeral representation

[Florian Haftmann]

Hi Brian,

> 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.

I have no strong opinion about that.  As it is now, theory »Code_Nat« is
not announced that prominently, but this is not that critical.

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

No.  Everything seems to be there.

All the best,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 262 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20120329/83041b0c/attachment.sig>