src/HOL/Word/Word.thy
2014-08-28 blanchet 2014-08-28 renamed new SMT module from 'SMT2' to 'SMT'
2014-08-28 blanchet 2014-08-28 moved old setup for SMT out
2014-08-28 blanchet 2014-08-28 removed needless, and for (newer versions of?) Haskell problematic code equations
2014-07-27 blanchet 2014-07-27 do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
2014-07-05 haftmann 2014-07-05 prefer ac_simps collections over separate name bindings for add and mult
2014-07-04 haftmann 2014-07-04 reduced name variants for assoc and commute on plus and mult
2014-06-11 Thomas Sewell 2014-06-11 Hypsubst preserves equality hypotheses Fixes included for various theories affected by this change.
2014-05-16 noschinl 2014-05-16 added lemmas for -1
2014-03-13 blanchet 2014-03-13 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
2014-03-06 blanchet 2014-03-06 renamed 'fun_rel' to 'rel_fun'
2014-03-02 wenzelm 2014-03-02 repaired document;
2014-03-01 haftmann 2014-03-01 more precise imports; avoid duplicated simp rules in fact collections; dropped redundancy
2014-03-01 haftmann 2014-03-01 earlier setup of transfer, without dependency on psychodelic interpretations
2014-03-01 haftmann 2014-03-01 cursory polishing: tuned proofs, tuned symbols, tuned headings
2014-02-12 blanchet 2014-02-12 renamed 'nat_{case,rec}' to '{case,rec}_nat'
2013-12-25 haftmann 2013-12-25 prefer more canonical names for lemmas on min/max
2013-12-23 haftmann 2013-12-23 prefer "Bits" as theory name for abstract bit operations, similar to "Orderings", "Lattices", "Groups" etc.
2013-12-23 haftmann 2013-12-23 dropped redundant lemma
2013-12-23 haftmann 2013-12-23 syntactically tuned
2013-12-23 haftmann 2013-12-23 prefer plain bool over dedicated type for binary digits
2013-12-14 wenzelm 2013-12-14 more antiquotations;
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