src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML
Thu, 15 Nov 2012 17:40:46 +0100 haftmann repaired slip accidentally introduced in 57209cfbf16b
Tue, 13 Nov 2012 09:08:32 +0100 haftmann prefer explicit Random.seed
Sun, 04 Dec 2011 20:05:08 +0100 bulwahn adding genuine flag to predicate_compile_quickcheck and prolog_quickcheck (cf. 5e46c225370e);
Mon, 14 Nov 2011 11:14:06 +0100 bulwahn setting up exhaustive generators which are used for the smart generators
Fri, 11 Nov 2011 12:10:49 +0100 bulwahn using more conventional names for monad plus operations
Fri, 11 Nov 2011 08:32:45 +0100 bulwahn adding CPS compilation to predicate compiler;
Thu, 20 Oct 2011 09:11:13 +0200 bulwahn modernizing predicate_compile_quickcheck
Wed, 17 Aug 2011 18:05:31 +0200 wenzelm modernized signature of Term.absfree/absdummy;
Mon, 18 Jul 2011 10:34:21 +0200 bulwahn adapting quickcheck based on the analysis of the predicate compiler
Sat, 16 Apr 2011 16:15:37 +0200 wenzelm modernized structure Proof_Context;
Wed, 30 Mar 2011 09:44:16 +0200 bulwahn generalizing compilation scheme of quickcheck generators to multiple arguments; changing random and exhaustive tester to use one code invocation for polymorphic instances with multiple cardinalities
Mon, 21 Mar 2011 08:29:16 +0100 bulwahn merged
Fri, 18 Mar 2011 18:19:42 +0100 bulwahn adapting predicate_compile_quickcheck; tuned
Sun, 20 Mar 2011 22:08:12 +0100 wenzelm simplified various cpu_time clones (!): eliminated odd Exn.capture/Exn.release (no need to "stop" timing);
Sun, 20 Mar 2011 21:28:11 +0100 wenzelm structure Timing: covers former start_timing/end_timing and Output.timeit etc;
Sat, 08 Jan 2011 17:14:48 +0100 wenzelm misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
Fri, 03 Dec 2010 08:40:47 +0100 bulwahn adapting predicate_compile_quickcheck
Mon, 25 Oct 2010 21:06:56 +0200 wenzelm renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
Fri, 22 Oct 2010 18:38:59 +0200 bulwahn adding generator quickcheck
Thu, 21 Oct 2010 19:13:11 +0200 bulwahn adapting alternative_defs, predicate_compile_quickcheck, examples and code_prolog
Tue, 28 Sep 2010 12:34:41 +0200 krauss consolidated tupled_lambda; moved to structure HOLogic
Mon, 20 Sep 2010 09:26:15 +0200 bulwahn removing clone in code_prolog and predicate_compile_quickcheck
Thu, 16 Sep 2010 16:51:33 +0200 haftmann adjusted to changes in Code_Runtime
Wed, 15 Sep 2010 15:40:35 +0200 haftmann Code_Runtime.value, corresponding to ML_Context.value
Wed, 15 Sep 2010 15:31:32 +0200 haftmann code_eval renamed to code_runtime
Wed, 15 Sep 2010 12:16:08 +0200 haftmann merged
Wed, 15 Sep 2010 11:30:32 +0200 haftmann replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references
Wed, 15 Sep 2010 09:36:39 +0200 bulwahn adding option show_invalid_clauses for a more detailed message when modes are not inferred
Wed, 15 Sep 2010 09:36:38 +0200 bulwahn proposed modes for code_pred now supports modes for mutual predicates
Thu, 09 Sep 2010 17:23:03 +0200 bulwahn removing report from the arguments of the quickcheck functions and refering to it by picking it from the context
Fri, 27 Aug 2010 12:57:55 +0200 wenzelm merged, resolving some minor conflicts in src/HOL/Tools/Predicate_Compile/code_prolog.ML;
Thu, 26 Aug 2010 20:51:17 +0200 haftmann formerly unnamed infix impliciation now named HOL.implies
Thu, 26 Aug 2010 12:06:00 +0200 wenzelm standardized Context.copy_thy to Theory.copy alias, with slightly more direct way of using it;
Thu, 19 Aug 2010 11:02:14 +0200 haftmann use antiquotations for remaining unqualified constants in HOL
Wed, 19 May 2010 18:24:07 +0200 bulwahn changing compilation to work only with contexts; adapting quickcheck
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;
Thu, 29 Apr 2010 15:00:41 +0200 haftmann dropped unnecessary ML code
Wed, 21 Apr 2010 12:10:52 +0200 bulwahn adopting quickcheck
Wed, 21 Apr 2010 12:10:52 +0200 bulwahn switched off no_topmost_reordering
Wed, 31 Mar 2010 16:44:41 +0200 bulwahn putting compilation setup of predicate compiler in a separate file
Mon, 29 Mar 2010 17:30:43 +0200 bulwahn made quickcheck generic with respect to which compilation; added random compilation to quickcheck
Mon, 22 Mar 2010 08:30:13 +0100 bulwahn reduced the debug output functions from 2 to 1
Tue, 02 Mar 2010 22:13:39 +0100 bulwahn made smlnj happy
Tue, 02 Mar 2010 22:13:33 +0100 bulwahn adding depth to predicate compile quickcheck for mutabelle tests; removing obsolete references in predicate compile quickcheck
Thu, 25 Feb 2010 14:01:34 +0100 bulwahn adopting Mutabelle to quickcheck reporting; improving quickcheck reporting
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
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
Mon, 07 Dec 2009 16:27:48 +0100 haftmann split off evaluation mechanisms in separte module Code_Eval
Thu, 19 Nov 2009 08:25:57 +0100 bulwahn replacing Predicate_Compile_Preproc_Const_Defs by more general Spec_Rules
Thu, 19 Nov 2009 08:25:47 +0100 bulwahn adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
Thu, 12 Nov 2009 20:39:02 +0100 bulwahn adding the predicate compiler quickcheck to the ex/ROOT.ML; adopting this quickcheck to the latest changes
Fri, 06 Nov 2009 08:18:35 +0100 bulwahn adopted the predicate compile quickcheck
Fri, 06 Nov 2009 08:11:58 +0100 bulwahn improved handling of overloaded constants; examples with numerals
Fri, 30 Oct 2009 09:55:15 +0100 bulwahn renamed rpred to random
Wed, 28 Oct 2009 00:07:51 +0100 wenzelm proper headers;
Tue, 27 Oct 2009 09:06:05 +0100 bulwahn added examples for quickcheck prototype
Tue, 27 Oct 2009 09:03:56 +0100 bulwahn adding a prototype of a counter-example generator based on the predicate compiler to HOL/ex
Tue, 27 Oct 2009 09:02:22 +0100 bulwahn including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
less more (0) tip