2010-02-23 bulwahn 2010-02-23 adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
2010-02-09 blanchet 2010-02-09 make Quickcheck identify itself, so people don't submit bug reports to me thinking that it was Nitpick
2010-01-20 bulwahn 2010-01-20 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
2009-12-18 blanchet 2009-12-18 made Quickcheck take structured proof assumptions into account (like Refute and Nitpick) by default; up to now, only Auto Quickcheck did -- the old behavior is available by passing "no_assms" as option
2009-11-10 blanchet 2009-11-10 merged, and renamed local "TheoryData" to "Data" (following common Isabelle conventions)
2009-10-29 blanchet 2009-10-29 merged
2009-10-28 blanchet 2009-10-28 introduced Auto Nitpick in addition to Auto Quickcheck; this required generalizing the theorem hook used by Quickcheck, following a suggestion by Florian
2009-10-28 blanchet 2009-10-28 use "get_goal" rather than "flat_goal" in Auto Quickcheck, since we don't need the extra facts for counterexample generation
2009-11-08 wenzelm 2009-11-08 adapted Theory_Data; tuned;
2009-10-28 wenzelm 2009-10-28 back to Proof.raw_goal;
2009-10-17 wenzelm 2009-10-17 indicate CRITICAL nature of various setmp combinators;
2009-10-02 wenzelm 2009-10-02 replaced Proof.get_goal state by Proof.flat_goal state, which provides the standard view on goals for (semi)automated tools;
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-07-31 boehmes 2009-07-31 Quickcheck callable from ML
2009-06-09 haftmann 2009-06-09 tuned make/map/merge combinators
2009-05-14 haftmann 2009-05-14 quickcheck size starts with 0
2009-05-13 haftmann 2009-05-13 dropped legacy operations
2009-04-25 wenzelm 2009-04-25 misc cleanup of auto_solve and quickcheck: tools are in src/Tools and loaded uniformly in HOL; preferences are configured in their proper place -- despite old misleading comments in the source; use predefined preferences categories; setmp preferences in-place;
2009-04-24 haftmann 2009-04-24 observe distinction between Pure/Tools and Tools more closely
2009-03-31 wenzelm 2009-03-31 fixed header;
2009-03-12 wenzelm 2009-03-12 Assumption.all_prems_of, Assumption.all_assms_of;
2008-12-31 wenzelm 2008-12-31 use regular Term.add_vars, Term.add_frees etc.; moved old add_term_vars, add_term_frees etc. to structure OldTerm;
2008-12-03 haftmann 2008-12-03 made repository layout more coherent with logical distribution structure; stripped some $Id$s