| Thu, 19 Aug 2010 11:02:14 +0200 |
haftmann |
use antiquotations for remaining unqualified constants in HOL
|
file |
diff |
annotate
|
| Wed, 19 May 2010 18:24:07 +0200 |
bulwahn |
changing compilation to work only with contexts; adapting quickcheck
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Thu, 29 Apr 2010 15:00:41 +0200 |
haftmann |
dropped unnecessary ML code
|
file |
diff |
annotate
|
| Wed, 21 Apr 2010 12:10:52 +0200 |
bulwahn |
adopting quickcheck
|
file |
diff |
annotate
|
| Wed, 21 Apr 2010 12:10:52 +0200 |
bulwahn |
switched off no_topmost_reordering
|
file |
diff |
annotate
|
| Wed, 31 Mar 2010 16:44:41 +0200 |
bulwahn |
putting compilation setup of predicate compiler in a separate file
|
file |
diff |
annotate
|
| Mon, 29 Mar 2010 17:30:43 +0200 |
bulwahn |
made quickcheck generic with respect to which compilation; added random compilation to quickcheck
|
file |
diff |
annotate
|
| Mon, 22 Mar 2010 08:30:13 +0100 |
bulwahn |
reduced the debug output functions from 2 to 1
|
file |
diff |
annotate
|
| Tue, 02 Mar 2010 22:13:39 +0100 |
bulwahn |
made smlnj happy
|
file |
diff |
annotate
|
| 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
|
file |
diff |
annotate
|
| Thu, 25 Feb 2010 14:01:34 +0100 |
bulwahn |
adopting Mutabelle to quickcheck reporting; improving quickcheck reporting
|
file |
diff |
annotate
|
| Thu, 25 Feb 2010 09:28:01 +0100 |
bulwahn |
added basic reporting of test cases to quickcheck
|
file |
diff |
annotate
|
| 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
|
file |
diff |
annotate
|
| 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
|
file |
diff |
annotate
|
| Mon, 07 Dec 2009 16:27:48 +0100 |
haftmann |
split off evaluation mechanisms in separte module Code_Eval
|
file |
diff |
annotate
|
| Thu, 19 Nov 2009 08:25:57 +0100 |
bulwahn |
replacing Predicate_Compile_Preproc_Const_Defs by more general Spec_Rules
|
file |
diff |
annotate
|
| Thu, 19 Nov 2009 08:25:47 +0100 |
bulwahn |
adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
|
file |
diff |
annotate
|
| 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
|
file |
diff |
annotate
|
| Fri, 06 Nov 2009 08:18:35 +0100 |
bulwahn |
adopted the predicate compile quickcheck
|
file |
diff |
annotate
|
| Fri, 06 Nov 2009 08:11:58 +0100 |
bulwahn |
improved handling of overloaded constants; examples with numerals
|
file |
diff |
annotate
|
| Fri, 30 Oct 2009 09:55:15 +0100 |
bulwahn |
renamed rpred to random
|
file |
diff |
annotate
|
| Wed, 28 Oct 2009 00:07:51 +0100 |
wenzelm |
proper headers;
|
file |
diff |
annotate
|
| Tue, 27 Oct 2009 09:06:05 +0100 |
bulwahn |
added examples for quickcheck prototype
|
file |
diff |
annotate
|
| 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
|
file |
diff |
annotate
|
| Tue, 27 Oct 2009 09:02:22 +0100 |
bulwahn |
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
|
file |
diff |
annotate
|