src/Tools/quickcheck.ML
Sat, 31 Jul 2010 21:14:20 +0200 ballarin Make registrations generic data.
Mon, 26 Jul 2010 14:44:07 +0200 haftmann quickcheck images of goals under registration morphisms
Wed, 21 Jul 2010 19:21:07 +0200 bulwahn adding checking of expected result for the tool quickcheck; annotated a few quickcheck examples
Wed, 21 Jul 2010 18:11:51 +0200 bulwahn correcting wellsortedness check and improving error message
Wed, 21 Jul 2010 18:11:51 +0200 bulwahn using multiple default types in quickcheck
Wed, 21 Jul 2010 18:11:51 +0200 bulwahn correcting merging of default_types
Wed, 21 Jul 2010 18:11:51 +0200 bulwahn reordering quickcheck signature; exporting test_params and inspection function
Wed, 21 Jul 2010 18:11:51 +0200 bulwahn changed default types to a list of types; extended quickcheck parameters to be a list of values to parse a list of default types
Mon, 17 May 2010 23:54:15 +0200 wenzelm prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
Mon, 03 May 2010 14:25:56 +0200 wenzelm renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
Sun, 07 Mar 2010 12:19:47 +0100 wenzelm modernized structure Object_Logic;
Thu, 25 Feb 2010 14:01:34 +0100 bulwahn adopting Mutabelle to quickcheck reporting; improving quickcheck reporting
Thu, 25 Feb 2010 10:04:50 +0100 bulwahn added quiet option to quickcheck command
Thu, 25 Feb 2010 09:28:01 +0100 bulwahn added basic reporting of test cases to quickcheck
Tue, 23 Feb 2010 13:36:15 +0100 bulwahn 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
Tue, 09 Feb 2010 16:05:49 +0100 blanchet make Quickcheck identify itself, so people don't submit bug reports to me thinking that it was Nitpick
Wed, 20 Jan 2010 11:56:45 +0100 bulwahn refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
Fri, 18 Dec 2009 14:02:58 +0100 blanchet made Quickcheck take structured proof assumptions into account (like Refute and Nitpick) by default;
Tue, 10 Nov 2009 13:54:00 +0100 blanchet merged, and renamed local "TheoryData" to "Data" (following common Isabelle conventions)
Thu, 29 Oct 2009 12:09:32 +0100 blanchet merged
Wed, 28 Oct 2009 17:43:43 +0100 blanchet introduced Auto Nitpick in addition to Auto Quickcheck;
Wed, 28 Oct 2009 11:55:48 +0100 blanchet use "get_goal" rather than "flat_goal" in Auto Quickcheck, since we don't need the extra facts for counterexample generation
Sun, 08 Nov 2009 18:43:42 +0100 wenzelm adapted Theory_Data;
Wed, 28 Oct 2009 22:04:57 +0100 wenzelm back to Proof.raw_goal;
Sat, 17 Oct 2009 15:57:51 +0200 wenzelm indicate CRITICAL nature of various setmp combinators;
Fri, 02 Oct 2009 22:02:11 +0200 wenzelm replaced Proof.get_goal state by Proof.flat_goal state, which provides the standard view on goals for (semi)automated tools;
Tue, 29 Sep 2009 16:24:36 +0200 wenzelm explicit indication of Unsynchronized.ref;
Fri, 31 Jul 2009 23:30:21 +0200 boehmes Quickcheck callable from ML
Tue, 09 Jun 2009 22:59:55 +0200 haftmann tuned make/map/merge combinators
Thu, 14 May 2009 15:09:46 +0200 haftmann quickcheck size starts with 0
Wed, 13 May 2009 18:41:40 +0200 haftmann dropped legacy operations
Sat, 25 Apr 2009 21:28:04 +0200 wenzelm misc cleanup of auto_solve and quickcheck:
Fri, 24 Apr 2009 17:45:17 +0200 haftmann observe distinction between Pure/Tools and Tools more closely
Tue, 31 Mar 2009 21:31:23 +0200 wenzelm fixed header;
Thu, 12 Mar 2009 15:54:58 +0100 wenzelm Assumption.all_prems_of, Assumption.all_assms_of;
Wed, 31 Dec 2008 00:08:13 +0100 wenzelm use regular Term.add_vars, Term.add_frees etc.;
Wed, 03 Dec 2008 15:58:44 +0100 haftmann made repository layout more coherent with logical distribution structure; stripped some $Id$s
less more (0) tip