2008-05-07 berghofe 2008-05-07 Deleted subset_antisym in a few proofs, because it is accidentally applied to predicates as well.
2008-04-04 haftmann 2008-04-04 more new primrec
2008-04-02 haftmann 2008-04-02 tuned towards code generation
2008-03-17 kleing 2008-03-17 fixed broken bintrunc lemma
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
2007-11-08 wenzelm 2007-11-08 eliminated illegal schematic variables in where/of; tuned;
2007-10-21 nipkow 2007-10-21 Eliminated most of the neq0_conv occurrences. As a result, many theorems had to be rephrased with ~= 0 instead of > 0.
2007-08-28 huffman 2007-08-28 revert to Word library version from 2007/08/20
2007-08-24 huffman 2007-08-24 remove unused lemmas
2007-08-23 huffman 2007-08-23 remove lemma bin_rec_PM
2007-08-23 huffman 2007-08-23 import BinInduct; remove constant bin_rl; remove redundant lemmas and definitions; clean up some proofs
2007-08-23 huffman 2007-08-23 move bin_nth stuff to its own subsection
2007-08-21 huffman 2007-08-21 move BIT datatype stuff from Num_Lemmas to BinGeneral
2007-08-21 huffman 2007-08-21 simplify termination proof
2007-08-20 huffman 2007-08-20 minimize imports
2007-08-20 huffman 2007-08-20 reorganize into subsections
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