src/HOL/Word/Word.thy
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
2011-12-23 huffman 2011-12-23 simplify some proofs
2011-12-23 huffman 2011-12-23 remove redundant lemma word_sub_def
2011-12-23 huffman 2011-12-23 remove two conflicting simp rules for 'number_of (number_of _)' pattern
2011-12-14 huffman 2011-12-14 replace 'lemmas' with 'lemma'
2011-12-13 huffman 2011-12-13 towards removing BIT_simps from the simpset
2011-12-12 huffman 2011-12-12 replace more uses of 'lemmas' with explicit 'lemma'; replace uses of 'simplified' attribute with 'unfolded'; remove unused intermediate lemmas.
2011-12-11 huffman 2011-12-11 replace many uses of 'lemmas' with 'lemma'; remove many unused intermediate lemmas.
2011-12-10 huffman 2011-12-10 prove class instances without extra lemmas
2011-12-10 huffman 2011-12-10 finite class instance for word type; remove unused lemmas
2011-12-10 huffman 2011-12-10 remove unused lemmas
2011-12-10 huffman 2011-12-10 generalize some lemmas
2011-12-10 huffman 2011-12-10 tidied Word.thy; put attributes directly on lemmas instead of using 'declare'; replace various 'lemmas' commands with ordinary 'lemma'.
2011-12-09 huffman 2011-12-09 remove redundant lemma word_diff_minus
2011-11-30 wenzelm 2011-11-30 prefer typedef without extra definition and alternative name; tuned proofs;
2011-11-23 wenzelm 2011-11-23 modernized some old-style infix operations, which were left over from the time of ML proof scripts;
2011-11-20 wenzelm 2011-11-20 eliminated obsolete "standard";
2011-11-18 huffman 2011-11-18 Word.thy: reduce usage of numeral-representation-dependent thms like number_of_is_id in proofs
2011-11-18 huffman 2011-11-18 merged
2011-11-17 huffman 2011-11-17 HOL-Word: removed more duplicate theorems
2011-11-17 huffman 2011-11-17 HOL-Word: removed many duplicate theorems (see NEWS)
2011-11-17 huffman 2011-11-17 Word.thy: rearrange to instantiate arithmetic classes together with arithmetic operations
2011-11-17 huffman 2011-11-17 move definitions of bitwise operators into appropriate document section
2011-11-17 wenzelm 2011-11-17 eliminated slightly odd Rep' with dynamically-scoped [simplified]; tuned 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-11-16 huffman 2011-11-16 simplify proof of word_of_int; remove several now-unused lemmas about Rep_Integ
2011-10-28 huffman 2011-10-28 use simproc_setup for cancellation simprocs, to get proper name bindings
2011-09-16 kleing 2011-09-16 removed word_neq_0_conv from simpset, it's almost never wanted.
2011-09-12 nipkow 2011-09-12 new fastforce replacing fastsimp - less confusing name
2011-09-07 huffman 2011-09-07 avoid using legacy theorem names
2011-09-07 wenzelm 2011-09-07 tuned proofs;
2011-05-13 wenzelm 2011-05-13 proper Proof.context for classical tactics; reduced claset to snapshot of classical context; discontinued clasimpset;
2011-01-14 wenzelm 2011-01-14 eliminated global prems; tuned proofs;
2010-12-29 wenzelm 2010-12-29 explicit file specifications -- avoid secondary load path;
2010-12-07 boehmes 2010-12-07 moved smt_word.ML into the directory of the Word library
2010-11-30 haftmann 2010-11-30 code preprocessor setup for numerals on word type; less meta-equalites; more xsymbols; less implicit propositions
2010-10-01 haftmann 2010-10-01 constant `contents` renamed to `the_elem`
2010-09-13 nipkow 2010-09-13 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
2010-09-07 nipkow 2010-09-07 expand_fun_eq -> ext_iff expand_set_eq -> set_ext_iff Naming in line now with multisets
2010-08-27 haftmann 2010-08-27 renamed class/constant eq to equal; tuned some instantiations
2010-08-18 haftmann 2010-08-18 moved spurious auxiliary lemma here
2010-07-19 haftmann 2010-07-19 diff_minus subsumes diff_def
2010-07-09 haftmann 2010-07-09 nicer xsymbol syntax for fcomp and scomp
2010-07-01 haftmann 2010-07-01 avoid bitstrings in generated code
2010-06-30 haftmann 2010-06-30 one unified Word theory