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 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 recursion combinator bin_rec; define AND for type int directly with function package
2011-12-28 huffman 2011-12-28 simplify definition of XOR for type int; reorder some lemmas
2011-12-28 huffman 2011-12-28 simplify definition of OR for type int; reorder some lemmas
2011-12-28 huffman 2011-12-28 simplify definition of NOT for type int
2011-12-28 huffman 2011-12-28 add several new tests, most of which don't work yet
2011-12-28 huffman 2011-12-28 fix typos
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-28 wenzelm 2011-12-28 disable kodkodi for now to prevent isatest failure of HOL-Nitpick_Examples due to 'a set constructor; prefer explicit version information;
2011-12-28 wenzelm 2011-12-28 updated platform information;
2011-12-28 wenzelm 2011-12-28 discontinued broken macbroy5 and thus the obsolete ppc-darwin platform;
2011-12-28 wenzelm 2011-12-28 more selective target "full" -- avoid failure of HOL-Datatype_Benchmark on 32bit platforms;
2011-12-28 wenzelm 2011-12-28 print case syntax depending on "show_cases" configuration option;
2011-12-27 huffman 2011-12-27 merged
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-27 huffman 2011-12-27 remove redundant syntax declaration
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-27 huffman 2011-12-27 declare word_of_int_{0,1} [simp], for consistency with word_of_int_bin
2011-12-27 haftmann 2011-12-27 be explicit about Finite_Set.fold
2011-12-27 haftmann 2011-12-27 dropped fact whose names clash with corresponding facts on canonical fold
2011-12-27 haftmann 2011-12-27 prefer canonical fold on lists
2011-12-27 haftmann 2011-12-27 be explicit about Finite_Set.fold
2011-12-26 haftmann 2011-12-26 incorporated More_Set and More_List into the Main body -- to be consolidated later
2011-12-26 haftmann 2011-12-26 moved theorem requiring multisets from More_List to Multiset
2011-12-26 haftmann 2011-12-26 NEWS: unavoidable fact renames
2011-12-26 haftmann 2011-12-26 dropped disfruitful `constant signatures`
2011-12-26 haftmann 2011-12-26 moved various set operations to theory Set (resp. Product_Type)
2011-12-26 haftmann 2011-12-26 dropped Executable_Set wrapper theory
2011-12-25 haftmann 2011-12-25 updated certificate
2011-12-24 haftmann 2011-12-24 NEWS: `set` is now a proper type constructor
2011-12-24 haftmann 2011-12-24 dropped references to obsolete facts `mem_def` and `Collect_def`
2011-12-24 haftmann 2011-12-24 dropped references to obsolete facts `mem_def_raw` and `Collect_def_raw`
2011-12-24 haftmann 2011-12-24 adjusted to set/pred distinction by means of type constructor `set`
2011-12-24 haftmann 2011-12-24 treatment of type constructor `set`
2011-12-24 haftmann 2011-12-24 executable intervals
2011-12-24 haftmann 2011-12-24 `set` is now a proper type constructor
2011-12-24 haftmann 2011-12-24 tuned layout
2011-12-24 haftmann 2011-12-24 reduced to a compatibility layer
2011-12-24 haftmann 2011-12-24 added setup for executable code
2011-12-24 haftmann 2011-12-24 moved `sublists` to theory Enum
2011-12-24 haftmann 2011-12-24 commented out examples which choke on strict set/pred distinction
2011-12-24 haftmann 2011-12-24 explicitly spelt out proof of equivariance avoids problem with automation due to type constructor `set`
2011-12-24 haftmann 2011-12-24 adjusted to set/pred distinction by means of type constructor `set`
2011-12-24 haftmann 2011-12-24 dropped references to obsolete fact `mem_def`
2011-12-24 haftmann 2011-12-24 dropped obsolete lemma member_set
2011-12-24 haftmann 2011-12-24 dropped obsolete code equation for Id