src/HOL/Word/Word.thy
2013-12-14 wenzelm 2013-12-14 proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.; clarified tool context in some boundary cases;
2013-11-19 haftmann 2013-11-19 eliminiated neg_numeral in favour of - (numeral _)
2013-10-31 haftmann 2013-10-31 generalized of_bool conversion
2013-10-31 haftmann 2013-10-31 separated bit operations on type bit from generic syntactic bit operations
2013-10-31 haftmann 2013-10-31 more lemmas on division
2013-08-18 wenzelm 2013-08-18 tuned;
2013-08-18 haftmann 2013-08-18 some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
2013-04-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
2013-03-08 kuncar 2013-03-08 patch Isabelle ditribution to conform to changes regarding the parametricity
2013-02-26 wenzelm 2013-02-26 tuned;
2013-02-15 haftmann 2013-02-15 two target language numeral types: integer and natural, as replacement for code_numeral; former theory HOL/Library/Code_Numeral_Types replaces HOL/Code_Numeral; refined stack of theories implementing int and/or nat by target language numerals; reduced number of target language numeral types to exactly one
2012-10-12 wenzelm 2012-10-12 discontinued obsolete typedef (open) syntax;
2012-08-22 wenzelm 2012-08-22 prefer ML_file over old uses;
2012-07-05 wenzelm 2012-07-05 explicit is better than implicit;
2012-05-18 kuncar 2012-05-18 don't generate code in Word because it breaks the current code setup
2012-04-19 huffman 2012-04-19 add code lemmas for word operations
2012-04-17 Thomas Sewell 2012-04-17 New tactic "word_bitwise" expands word equalities/inequalities into logic.
2012-04-18 kuncar 2012-04-18 setup_lifting: no_code switch and supoport for quotient theorems
2012-04-17 kuncar 2012-04-17 tuned the setup of lifting; generate transfer rules for typedef and Quotient thms
2012-04-06 huffman 2012-04-06 remove now-unnecessary type annotations from lift_definition commands
2012-04-05 huffman 2012-04-05 use standard quotient lemmas to generate transfer rules
2012-04-05 huffman 2012-04-05 set up and use lift_definition for word operations
2012-04-05 huffman 2012-04-05 configure transfer method for 'a word -> int
2012-03-27 huffman 2012-03-27 mark some duplicate lemmas for deletion
2012-03-25 huffman 2012-03-25 merged fork with new numeral representation (see NEWS)
2012-03-16 huffman 2012-03-16 make more word theorems respect int/bin distinction
2012-02-24 huffman 2012-02-24 remove ill-formed lemmas word_0_wi_Pls and word_m1_wi_Min
2012-02-24 huffman 2012-02-24 avoid using Int.succ or Int.pred in proofs
2012-02-24 huffman 2012-02-24 avoid using Int.Pls_def in proofs
2012-02-24 huffman 2012-02-24 remove ill-formed lemmas word_pred_0_Min and word_m1_Min
2012-02-24 huffman 2012-02-24 remove ill-formed lemma of_bl_no; adapt proofs
2012-02-24 huffman 2012-02-24 adapt lemma mask_lem to respect int/bin distinction
2012-02-23 huffman 2012-02-23 make more simp rules respect int/bin distinction
2012-02-23 huffman 2012-02-23 make bool list functions respect int/bin distinction
2012-02-23 huffman 2012-02-23 make uses of bin_sign respect int/bin distinction
2012-02-23 huffman 2012-02-23 removed unnecessary lemma zero_bintrunc
2012-02-23 huffman 2012-02-23 remove unnecessary lemmas
2012-02-08 blanchet 2012-02-08 use 'primrec' to define "rotate1", for uniformity (and to help first-order tools that rely on "Spec_Rules")
2012-01-10 huffman 2012-01-10 add simp rules for set_bit and msb applied to 0 and 1
2012-01-10 huffman 2012-01-10 add simp rule test_bit_1
2012-01-06 wenzelm 2012-01-06 recovered case syntax for of_int, also with source positions (appears to be unused nonetheless);
2012-01-05 wenzelm 2012-01-05 misc tuning;
2011-12-30 huffman 2011-12-30 add simp rules for bitwise word operations with 1
2011-12-30 huffman 2011-12-30 remove unnecessary intermediate lemmas
2011-12-29 haftmann 2011-12-29 semiring_numeral_0_eq_0, semiring_numeral_1_eq_1 now [simp], superseeding corresponding simp rules on type nat
2011-12-28 wenzelm 2011-12-28 merged
2011-12-28 huffman 2011-12-28 restate some lemmas to respect int/bin distinction
2011-12-28 huffman 2011-12-28 simplify some proofs
2011-12-28 huffman 2011-12-28 add lemma word_eq_iff
2011-12-28 huffman 2011-12-28 restate lemma word_1_no in terms of Numeral1
2011-12-28 huffman 2011-12-28 remove some duplicate lemmas
2011-12-28 huffman 2011-12-28 simplify proof
2011-12-28 huffman 2011-12-28 replace 'lemmas' with explicit 'lemma'
2011-12-28 huffman 2011-12-28 add section headings
2011-12-27 huffman 2011-12-27 remove duplicate lemma lists
2011-12-28 wenzelm 2011-12-28 reverted some changes for set->predicate transition, according to "hg log -u berghofe -r Isabelle2007:Isabelle2008"; tuned proofs;
2011-12-27 huffman 2011-12-27 redefine some binary operations on integers work on abstract numerals instead of Int.Pls and Int.Min
2011-12-27 huffman 2011-12-27 remove some uses of Int.succ and Int.pred
2011-12-27 huffman 2011-12-27 remove redundant syntax declaration
2011-12-27 huffman 2011-12-27 declare word_of_int_{0,1} [simp], for consistency with word_of_int_bin