* 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