[isabelle-dev] NEWS: numeral representation

Brian Huffman huffman at in.tum.de
Thu Mar 29 08:29:10 CEST 2012


On Thu, Mar 29, 2012 at 7:50 AM, Florian Haftmann
<florian.haftmann at informatik.tu-muenchen.de> wrote:
> As it is now, theory »Code_Nat« is
> not announced that prominently, but this is not that critical.

We should at least put an announcement in NEWS about Code_Nat.

However, you have talked about making the binary representation for
"nat" the default in HOL-Main, i.e. merging Code_Nat into the Nat/Num
theories. Are you still interested in doing this?

- Brian



More information about the isabelle-dev mailing list