2010-02-02 boehmes 2010-02-02 updated dependencies
2010-02-02 boehmes 2010-02-02 merged
2010-02-02 boehmes 2010-02-02 updated SMT certificates
2010-02-02 boehmes 2010-02-02 updated examples due to changes in the way SMT certificates are stored
2010-02-02 berghofe 2010-02-02 merged
2010-01-31 berghofe 2010-01-31 merged
2010-01-30 berghofe 2010-01-30 Adapted to changes in cases method.
2010-01-30 berghofe 2010-01-30 Adapted to changes in setup of cases method.
2010-01-30 berghofe 2010-01-30 Added setup for simplification of equality constraints in cases rules.
2010-01-30 berghofe 2010-01-30 Added infrastructure for simplifying equality constraints in cases rules.
2010-01-30 berghofe 2010-01-30 Added "constraints" tag / attribute for specifying the number of equality constraints in cases rules.
2010-02-02 boehmes 2010-02-02 updated SMT certificates
2010-02-02 boehmes 2010-02-02 updated SMT examples
2010-02-02 boehmes 2010-02-02 collect certificates in a single file
2010-02-02 blanchet 2010-02-02 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
2010-02-01 himmelma 2010-02-01 Removed explicit type annotations
2010-01-31 haftmann 2010-01-31 adjusted to changes in List_Set.thy
2010-01-31 haftmann 2010-01-31 more correspondence lemmas between related operations
2010-01-31 haftmann 2010-01-31 canonical insert operation; generalized lemma foldl_apply_inv to foldl_apply
2010-01-31 haftmann 2010-01-31 dropped some redundancies
2010-01-31 haftmann 2010-01-31 generalized lemma foldl_apply_inv to foldl_apply
2010-01-31 haftmann 2010-01-31 more correspondence lemmas between related operations; tuned some proofs
2010-01-28 haftmann 2010-01-28 new theory Algebras.thy for generic algebraic structures
2010-01-28 haftmann 2010-01-28 dropped mk_left_commute; use interpretation of locale abel_semigroup instead
2010-01-27 haftmann 2010-01-27 merged
2010-01-27 haftmann 2010-01-27 a more complex record expression -- cf. src/HOL/Tools/quickcheck_generators.ML
2010-01-27 haftmann 2010-01-27 lemma Image_closed_trancl
2010-01-27 haftmann 2010-01-27 corrected type of typecopy constructor
2010-01-27 haftmann 2010-01-27 tuned structure; moved non-related quickcheck.setup to Code_Generator.thy
2010-01-27 berghofe 2010-01-27 Changed author; removed debugging code.
2010-01-25 bulwahn 2010-01-25 merged
2010-01-25 bulwahn 2010-01-25 adding Mutabelle to repository
2010-01-25 hoelzl 2010-01-25 Replaced vec1 and dest_vec1 by abbreviation.
2010-01-22 haftmann 2010-01-22 merged
2010-01-22 haftmann 2010-01-22 HOLogic.strip_psplits: types are ordered after syntactic appearance, not after corresponding de-Bruin index (closer correspondence to similar strip operations)
2010-01-22 boehmes 2010-01-22 merged
2010-01-22 boehmes 2010-01-22 support skolem constant for extensional arrays in Z3 proofs
2010-01-22 boehmes 2010-01-22 drop underscores at end of names coming from Boogie
2010-01-22 bulwahn 2010-01-22 merged
2010-01-22 bulwahn 2010-01-22 correctly hiding facts of Lazy_Sequence
2010-01-21 bulwahn 2010-01-21 corrected and simplified Spec_Rules registration in the Recdef package
2010-01-21 bulwahn 2010-01-21 merged
2010-01-21 bulwahn 2010-01-21 adopting predicate compiler to new Spec_Rules and eliminating the use of Nitpick_Simps
2010-01-20 bulwahn 2010-01-20 adopting Sequences
2010-01-20 bulwahn 2010-01-20 added registration of equational theorems from prim_rec and rec_def to Spec_Rules
2010-01-20 bulwahn 2010-01-20 merged
2010-01-18 krauss 2010-01-18 function package: declare Spec_Rules for simps from total functions, but not psimps or tail-rec equations
2010-01-20 bulwahn 2010-01-20 merged
2010-01-20 bulwahn 2010-01-20 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
2010-01-22 haftmann 2010-01-22 simplified proofs
2010-01-22 haftmann 2010-01-22 NEWS
2010-01-22 haftmann 2010-01-22 more accurate dependencies
2010-01-22 haftmann 2010-01-22 code literals: distinguish numeral classes by different entries
2010-01-22 haftmann 2010-01-22 cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
2010-01-21 haftmann 2010-01-21 merged
2010-01-16 haftmann 2010-01-16 dropped some old primrecs and some constdefs
2010-01-16 haftmann 2010-01-16 explicit CONST in translations
2010-01-16 haftmann 2010-01-16 modernized syntax
2010-01-20 blanchet 2010-01-20 fix issues with previous Nitpick change
2010-01-20 blanchet 2010-01-20 merged