[isabelle-dev] NEWS

[Brian Huffman]

* Theory Int: The representation of numerals has changed.  The infix operator
BIT and the bit datatype with constructors B0 and B1 have disappeared.
INCOMPATIBILITY, use "Int.Bit0 x" and "Int.Bit1 y" in place of "x BIT bit.B0"
and "y BIT bit.B1", respectively.  Theorems involving BIT, B0, or B1 have been
renamed with "Bit0" or "Bit1" accordingly.


(I have moved the definitions of op BIT and the bit datatype into the  
HOL-Word library, for backward compatibility there. Lemmas involving  
BIT are now proved in both styles, and the simplifier rewrites  
applications of BIT to B0 or B1 to Bit0 or Bit1 by default. In  
theories using HOL-Word, lemmas explicitly mentioning BIT may still  
work, but I would recommend switching over to the new-style Bit0 and  
Bit1. Please let me know if this causes any problems with applications  
using HOL-Word.)

- Brian