2009-01-28 nipkow 2009-01-28 merged - resolving conflics
2009-01-28 nipkow 2009-01-28 Replaced group_ and ring_simps by algebra_simps; removed compare_rls - use algebra_simps now
2009-01-26 haftmann 2009-01-26 stripped Id
2008-09-19 huffman 2008-09-19 avoid using implicit assumptions
2008-08-29 haftmann 2008-08-29 fixed names of class assumptions
2008-07-21 haftmann 2008-07-21 (re-)added simp rules for (_ + _) div/mod _
2008-07-18 haftmann 2008-07-18 moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
2008-06-10 haftmann 2008-06-10 slightly tuning of some proofs involving case distinction and induction on natural numbers and similar
2008-04-09 huffman 2008-04-09 move lemmas from Word/BinBoolList.thy to List.thy
2008-04-04 haftmann 2008-04-04 more new primrec
2008-02-17 huffman 2008-02-17 New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
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-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-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-22 huffman 2007-08-22 move if_simps from BinBoolList to Num_Lemmas
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 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