2009-01-26 haftmann 2009-01-26 stripped Id
2008-10-10 haftmann 2008-10-10 `code func` now just `code`
2008-08-28 krauss 2008-08-28 more function -> fun
2008-04-04 haftmann 2008-04-04 renamed app2 to map2
2008-04-02 haftmann 2008-04-02 tuned towards code generation
2008-02-17 huffman 2008-02-17 New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
2008-01-15 haftmann 2008-01-15 joined theories IntDef, Numeral, IntArith to theory Int
2008-01-02 haftmann 2008-01-02 splitted class uminus from class minus
2007-10-20 chaieb 2007-10-20 fixed proofs
2007-08-28 huffman 2007-08-28 revert to Word library version from 2007/08/20
2007-08-24 huffman 2007-08-24 bin_sc_nth proof
2007-08-23 huffman 2007-08-23 avoid use of bin_rec_PM
2007-08-22 huffman 2007-08-22 move bool list stuff from BinOperations to BinBoolList; reorganize BinBoolList into subsections
2007-08-20 huffman 2007-08-20 AC rules for bitwise logical operators no longer declared simp
2007-08-20 huffman 2007-08-20 move bit simps from BinOperations to BitSyntax
2007-08-20 huffman 2007-08-20 reorganize into subsections
2007-08-20 huffman 2007-08-20 use overloaded bitwise operators at type int
2007-08-20 huffman 2007-08-20 headers for document generation
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