src/HOL/Word/Bool_List_Representation.thy
2017-04-03 wenzelm 2017-04-03 misc tuning and modernization;
2016-11-19 wenzelm 2016-11-19 avoid import of Complex_Main into Word library (amending 34b7e2da95f6), e.g. to avoid intrusion of const "ii" into theories without complex numbers;
2016-08-10 nipkow 2016-08-10 "split add" -> "split"
2016-07-15 eberlm 2016-07-15 Tuned Bool_List_Representation
2016-04-12 wenzelm 2016-04-12 tuned;
2016-03-23 kleing 2016-03-23 HOL-Word: add stronger bl_to_bin_lt2p_drop
2016-02-23 nipkow 2016-02-23 more canonical names
2015-12-07 wenzelm 2015-12-07 isabelle update_cartouches -c -t;
2015-10-13 haftmann 2015-10-13 prod_case as canonical name for product type eliminator
2014-11-02 wenzelm 2014-11-02 modernized header;
2014-09-21 haftmann 2014-09-21 explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
2014-07-05 haftmann 2014-07-05 prefer ac_simps collections over separate name bindings for add and mult
2014-06-11 Thomas Sewell 2014-06-11 Hypsubst preserves equality hypotheses Fixes included for various theories affected by this change.
2014-03-13 nipkow 2014-03-13 enhanced simplifier solver for preconditions of rewrite rule, can now deal with conjunctions
2013-12-28 haftmann 2013-12-28 move instantiation here from AFP/Native_Word
2013-12-28 haftmann 2013-12-28 cleanup
2013-12-27 haftmann 2013-12-27 tuned proofs and declarations
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 syntactically tuned
2013-12-23 haftmann 2013-12-23 prefer plain bool over dedicated type for binary digits
2013-09-06 haftmann 2013-09-06 slight cleanup of lemma locations; tuned proof
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
2012-03-30 huffman 2012-03-30 restate various simp rules for word operations using pred_numeral
2012-03-25 huffman 2012-03-25 merged fork with new numeral representation (see NEWS)
2012-02-24 huffman 2012-02-24 avoid using Int.succ_def in proofs
2012-02-24 huffman 2012-02-24 avoid using BIT_simps in proofs; rephrase lemmas without Int.succ or Int.pred;
2012-02-24 huffman 2012-02-24 avoid using BIT_simps in 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 bool list functions respect int/bin distinction
2012-01-17 huffman 2012-01-17 factor-cancellation simprocs now call the full simplifier to prove that factors are non-zero
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 use 'induct arbitrary' instead of 'rule_format' attribute
2011-12-27 huffman 2011-12-27 declare simp rules immediately, instead of using 'declare' commands
2011-12-13 huffman 2011-12-13 replace many uses of 'lemmas' with explicit 'lemma'
2011-12-13 huffman 2011-12-13 towards removing BIT_simps from the simpset
2011-12-13 huffman 2011-12-13 remove some unwanted numeral-representation-specific simp rules
2011-11-20 wenzelm 2011-11-20 eliminated obsolete "standard";
2011-11-17 huffman 2011-11-17 HOL-Word: add simp rules for bin_rest, bin_last; shorten several proofs
2011-11-12 huffman 2011-11-12 removed some old-style semicolons
2011-09-16 kleing 2011-09-16 removed unused legacy lemma names, some comment cleanup.
2011-02-25 nipkow 2011-02-25 added simp lemma nth_Cons_pos to List
2010-07-01 haftmann 2010-07-01 avoid bitstrings in generated code
2010-06-30 haftmann 2010-06-30 more speaking names