src/HOL/Word/BitSyntax.thy
2008-04-04 haftmann 2008-04-04 syntactic classes for bit operations
2008-02-17 huffman 2008-02-17 New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
2008-01-02 haftmann 2008-01-02 splitted class uminus from class minus
2007-11-10 wenzelm 2007-11-10 tuned specifications of 'notation';
2007-08-20 huffman 2007-08-20 move bit simps from BinOperations to BitSyntax
2007-08-20 huffman 2007-08-20 use class instead of axclass
2007-08-20 kleing 2007-08-20 added header
2007-08-20 kleing 2007-08-20 * HOL-Word: New extensive library and type for generic, fixed size machine words, with arithemtic, bit-wise, shifting and rotating operations, reflection into int, nat, and bool lists, automation for linear arithmetic (by automatic reflection into nat or int), including lemmas on overflow and monotonicity. Instantiated to all appropriate arithmetic type classes, supporting automatic simplification of numerals on all operations. Jointly developed by NICTA, Galois, and PSU. * still to do: README.html/document + moving some of the generic lemmas to appropriate place in distribution