src/HOL/Word/WordDefinition.thy
2008-06-10 wenzelm 2008-06-10 back to original import order -- thanks to proper deletion of nat cases/induct rules from type_definition;
2008-06-10 wenzelm 2008-06-10 reordering of imports ensures that nat_induct stay in front;
2008-04-08 kleing 2008-04-08 removed abbrev for word_power. Was in the wrong direction and unused.
2008-04-04 haftmann 2008-04-04 syntactic classes for bit operations
2008-04-02 haftmann 2008-04-02 tuned towards code generation
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-11-08 wenzelm 2007-11-08 eliminated illegal schematic variables in where/of; tuned;
2007-10-22 wenzelm 2007-10-22 fixed proof: no one_is_Suc_zero;
2007-08-28 huffman 2007-08-28 revert to Word library version from 2007/08/20
2007-08-23 huffman 2007-08-23 new instance proofs
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 bool list stuff from WordDefinition and WordArith to new WordBoolList theory
2007-08-21 huffman 2007-08-21 move udvd, div and mod stuff from WordDefinition to WordArith
2007-08-21 huffman 2007-08-21 move order-related stuff from WordDefinition to WordArith
2007-08-21 huffman 2007-08-21 move scast/ucast stuff to its own subsection
2007-08-21 huffman 2007-08-21 move shifting-related constant definitions from WordDefinition to WordShift
2007-08-20 huffman 2007-08-20 minimize imports
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