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

Attachment: signature.asc
Description: OpenPGP digital signature

_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Reply via email to