brianh at cs.pdx.edu
Sun Feb 17 07:08:41 CET 2008
* 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
More information about the isabelle-dev