src/HOL/Word/Bit_Representation.thy
2014-10-30 haftmann 2014-10-30 more simp rules concerning dvd and even/odd
2014-10-09 haftmann 2014-10-09 more foundational definition for predicate even
2014-09-21 haftmann 2014-09-21 explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
2013-12-28 haftmann 2013-12-28 dropped junk
2013-12-25 haftmann 2013-12-25 prefer more canonical names for lemmas on min/max
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-11-19 haftmann 2013-11-19 eliminiated neg_numeral in favour of - (numeral _)
2013-11-01 haftmann 2013-11-01 more simplification rules on unary and binary minus
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-27 huffman 2012-03-27 remove unused premises
2012-03-27 huffman 2012-03-27 mark some duplicate lemmas for deletion
2012-03-27 huffman 2012-03-27 generalized lemma zpower_zmod
2012-03-27 huffman 2012-03-27 remove redundant lemma
2012-03-25 huffman 2012-03-25 merged fork with new numeral representation (see NEWS)
2012-02-23 huffman 2012-02-23 remove duplicate lemma bintrunc_Suc in favor of bintrunc.Suc
2012-02-23 huffman 2012-02-23 remove unused lemmas
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 constant bin_rl
2012-02-23 huffman 2012-02-23 remove duplication of lemmas bin_{rest,last}_BIT
2012-02-23 huffman 2012-02-23 remove lemmas Bit{0,1}_div2
2012-02-23 huffman 2012-02-23 simplify proof
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 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 removed unused lemmas
2011-12-23 huffman 2011-12-23 use 'induct arbitrary' instead of universal quantifiers
2011-12-23 huffman 2011-12-23 remove two conflicting simp rules for 'number_of (number_of _)' pattern
2011-12-22 huffman 2011-12-22 add lemma bin_nth_minus1
2011-12-13 huffman 2011-12-13 more simp rules for sbintrunc
2011-12-13 huffman 2011-12-13 add simp rules for sbintrunc applied to numerals
2011-12-13 huffman 2011-12-13 add lemma bin_nth_zero
2011-12-13 huffman 2011-12-13 add simp rules for bintrunc applied to numerals
2011-12-13 huffman 2011-12-13 add simp rules for bin_rest and bin_last applied to numerals
2011-12-13 huffman 2011-12-13 add simp rules for bin_sign applied to numerals
2011-12-13 huffman 2011-12-13 add simp rules for BIT applied to numerals
2011-12-13 huffman 2011-12-13 declare BIT_eq_iff [iff]; remove unneeded lemmas
2011-12-13 huffman 2011-12-13 towards removing BIT_simps from the simpset
2011-12-13 huffman 2011-12-13 type signature for bin_sign
2011-12-13 huffman 2011-12-13 remove some unwanted numeral-representation-specific simp rules
2011-12-13 huffman 2011-12-13 remove redundant lemmas
2011-12-13 huffman 2011-12-13 reorder some definitions and proofs, in preparation for new numeral representation
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-16 huffman 2011-11-16 remove redundant lemmas bin_last_mod and bin_rest_div, use bin_last_def and bin_rest_def instead
2011-09-16 kleing 2011-09-16 removed unused legacy lemma names, some comment cleanup.
2011-09-12 nipkow 2011-09-12 new fastforce replacing fastsimp - less confusing name
2010-12-29 wenzelm 2010-12-29 explicit file specifications -- avoid secondary load path;
2010-07-01 haftmann 2010-07-01 avoid bitstrings in generated code
2010-06-30 haftmann 2010-06-30 more speaking names