2009-02-21 nipkow 2009-02-21 Removed subsumed lemmas
2009-01-26 haftmann 2009-01-26 stripped Id
2008-10-20 nipkow 2008-10-20 fixed proof
2008-06-10 wenzelm 2008-06-10 recovered nat_induct as default for induct_tac;
2008-06-10 wenzelm 2008-06-10 case_tac: accomodate change in bound variable name;
2008-05-17 wenzelm 2008-05-17 avoid undeclared variables in facts;
2008-04-04 haftmann 2008-04-04 renamed app2 to map2
2008-03-15 wenzelm 2008-03-15 avoid unclear fact references;
2008-02-17 huffman 2008-02-17 New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
2008-02-15 haftmann 2008-02-15 <= and < on nat no longer depend on wellfounded relations
2008-01-28 wenzelm 2008-01-28 eliminated escaped white space;
2008-01-15 haftmann 2008-01-15 joined theories IntDef, Numeral, IntArith to theory Int
2007-11-08 wenzelm 2007-11-08 eliminated illegal schematic variables in where/of;
2007-08-28 huffman 2007-08-28 revert to Word library version from 2007/08/20
2007-08-22 huffman 2007-08-22 removed Word/Size.thy; replaced len_of TYPE('a) with CARD('a); replaced axclass len with class finite; replaced axclass len0 with class type
2007-08-22 huffman 2007-08-22 move constant definitions to their respective subsections
2007-08-22 huffman 2007-08-22 move bool list operations from WordBitwise to WordBoolList
2007-08-21 huffman 2007-08-21 move shifting-related constant definitions from WordDefinition to WordShift
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