src/HOL/Word/TdThs.thy
2009-01-26 haftmann 2009-01-26 stripped Id
2008-12-15 ballarin 2008-12-15 More porting to new locales.
2008-06-10 wenzelm 2008-06-10 proper deletion of nat cases/induct rules from type_definition;
2008-06-10 wenzelm 2008-06-10 more robust declaration of nat_induct;
2008-04-04 haftmann 2008-04-04 tuned
2007-11-02 kleing 2007-11-02 Added reference to Jeremy Dawson's paper on the word library. Added header to remaining word/*.thy files so they show up in toc.
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