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
2011-12-24 haftmann 2011-12-24 tuned proofs
2011-12-24 haftmann 2011-12-24 generalized type signature to permit overloading on `set`
2011-12-24 haftmann 2011-12-24 added monad instance for `set`
2011-12-24 haftmann 2011-12-24 enum type class instance for `set`; dropped misfitting code lemma for trancl
2011-12-24 haftmann 2011-12-24 finite type class instance for `set`
2011-12-24 haftmann 2011-12-24 treatment of type constructor `set`
2011-12-24 haftmann 2011-12-24 lattice type class instances for `set`; added code lemma for Set.bind
2011-12-24 haftmann 2011-12-24 `set` is now a proper type constructor; added operation for set monad
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 add lemmas bin_cat_zero and bin_split_zero
2011-12-23 huffman 2011-12-23 more uses of 'induct arbitrary'
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-21 blanchet 2011-12-21 removed killed encoding from example
2011-12-21 blanchet 2011-12-21 updated docs
2011-12-21 blanchet 2011-12-21 killed "guard@?" encodings -- they were found to be unsound
2011-12-21 blanchet 2011-12-21 extend previous optimizations to guard-based encodings
2011-12-21 blanchet 2011-12-21 treat polymorphic constructors specially in @? encodings
2011-12-21 blanchet 2011-12-21 tuning
2011-12-21 blanchet 2011-12-21 no need for type arguments for monomorphic constructors of polymorphic datatypes (e.g. "Nil")
2011-12-21 bulwahn 2011-12-21 added some basic documentation about method induction_schema extracted from old NEWS
2011-12-21 bulwahn 2011-12-21 adding documentation about the quickcheck_generator command in the IsarRef
2011-12-21 bulwahn 2011-12-21 extending quickcheck example
2011-12-21 bulwahn 2011-12-21 NEWS
2011-12-21 bulwahn 2011-12-21 quickcheck_generator command also creates random generators
2011-12-20 blanchet 2011-12-20 don't try to avoid SPASS keywords; instead, just suffix an underscore to all generated identifiers
2011-12-20 blanchet 2011-12-20 one more SPASS identifier
2011-12-20 blanchet 2011-12-20 tuning
2011-12-20 noschinl 2011-12-20 merged
2011-12-17 traytel 2011-12-17 meaningful error message on failing merges of coercion tables