src/HOL/Library/Word.thy
2009-03-03 nipkow 2009-03-03 removed and renamed redundant lemmas
2008-10-10 haftmann 2008-10-10 `code func` now just `code`
2008-09-16 haftmann 2008-09-16 dropped superfluous code lemmas
2008-07-07 haftmann 2008-07-07 absolute imports of HOL/*.thy theories
2008-06-26 haftmann 2008-06-26 established Plain theory and image
2008-06-10 haftmann 2008-06-10 removed some dubious code lemmas
2008-03-29 wenzelm 2008-03-29 purely functional setup of claset/simpset/clasimpset;
2008-02-17 huffman 2008-02-17 New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
2008-01-25 haftmann 2008-01-25 moved definition of power on ints to theory Int
2008-01-15 haftmann 2008-01-15 joined theories IntDef, Numeral, IntArith to theory Int
2007-12-10 haftmann 2007-12-10 switched import from Main to List
2007-10-23 nipkow 2007-10-23 went back to >0
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-07-17 krauss 2007-07-17 reverted fun->recdef, since there are problems with induction rule
2007-07-16 krauss 2007-07-16 use function package
2007-06-23 nipkow 2007-06-23 tuned and renamed group_eq_simps and ring_eq_simps
2007-06-20 huffman 2007-06-20 change simp rules for of_nat to work like int did previously (reorient of_nat_Suc, remove of_nat_mult [simp]); preserve original variable names in legacy int theorems
2007-06-13 wenzelm 2007-06-13 tuned proofs: avoid implicit prems; major cleanup of proofs/document;
2007-06-13 huffman 2007-06-13 removed constant int :: nat => int; int is now an abbreviation for of_nat :: nat => int
2007-05-17 haftmann 2007-05-17 tuned
2007-01-11 paulson 2007-01-11 well-founded relations for the integers
2006-11-17 wenzelm 2006-11-17 more robust syntax for definition/abbreviation/notation;
2006-11-07 wenzelm 2006-11-07 renamed 'const_syntax' to 'notation';
2006-09-06 haftmann 2006-09-06 got rid of Numeral.bin type
2006-07-26 webertj 2006-07-26 linear arithmetic splits certain operators (e.g. min, max, abs)
2006-05-27 wenzelm 2006-05-27 tuned;
2005-09-26 skalberg 2005-09-26 Made sure all lemmas now have names (especially so that certain of them can be removed from the simpset).
2005-07-13 paulson 2005-07-13 generlization of some "nat" theorems
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2005-03-23 paulson 2005-03-23 replaced bool by a new datatype "bit" for binary numerals
2005-02-02 paulson 2005-02-02 tidying of some subst/simplesubst proofs
2005-02-01 paulson 2005-02-01 the new subst tactic, by Lucas Dixon
2004-11-24 berghofe 2004-11-24 Functions nat_to_bv and bv_to_nat now really operate on natural numbers.
2004-08-18 nipkow 2004-08-18 import -> imports
2004-08-16 nipkow 2004-08-16 New theory header syntax.
2004-07-20 paulson 2004-07-20 removed some obsolete proofs
2004-07-01 paulson 2004-07-01 new treatment of binary numerals
2004-05-06 wenzelm 2004-05-06 tuned document;
2004-04-16 wenzelm 2004-04-16 tuned document;
2004-04-14 kleing 2004-04-14 use more symbols in HTML output
2004-03-29 skalberg 2004-03-29 Added bitvector library (Word) to HOL/Library and a theory using it (Adder) to HOL/ex.