src/HOL/Word/Num_Lemmas.thy
2009-03-04 blanchet 2009-03-04 Merge.
2009-03-04 blanchet 2009-03-04 Merge.
2009-03-02 nipkow 2009-03-02 name changes
2009-02-21 nipkow 2009-02-21 Removed subsumed lemmas
2009-02-21 nipkow 2009-02-21 removed redundant thms
2009-02-20 nipkow 2009-02-20 Removed redundant lemmas
2009-02-17 nipkow 2009-02-17 Cleaned up IntDiv and removed subsumed lemmas.
2008-12-03 haftmann 2008-12-03 made repository layout more coherent with logical distribution structure; stripped some $Id$s
2008-07-18 haftmann 2008-07-18 moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
2008-07-14 chaieb 2008-07-14 Simplified proofs
2008-04-04 haftmann 2008-04-04 tuned
2008-04-02 haftmann 2008-04-02 tuned towards code generation
2008-03-17 huffman 2008-03-17 remove unneeded constant mod_alt
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-21 haftmann 2008-01-21 tuned proof
2008-01-15 haftmann 2008-01-15 joined theories IntDef, Numeral, IntArith to theory Int
2008-01-09 nipkow 2008-01-09 added simp attributes/ proofs fixed
2007-12-10 haftmann 2007-12-10 explicit import of theory Main
2007-11-08 wenzelm 2007-11-08 eliminated illegal schematic variables in where/of; tuned;
2007-08-28 huffman 2007-08-28 revert to Word library version from 2007/08/20
2007-08-23 huffman 2007-08-23 remove unused lemmas
2007-08-22 huffman 2007-08-22 move if_simps from BinBoolList to Num_Lemmas
2007-08-21 huffman 2007-08-21 remove redundant lemmas
2007-08-21 huffman 2007-08-21 move BIT datatype stuff from Num_Lemmas to BinGeneral
2007-08-20 huffman 2007-08-20 remove redundant lemma int_number_of
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