| Fri, 11 Mar 2011 08:58:29 +0100 |
bulwahn |
removing debug message in quickcheck's postprocessor
|
file |
diff |
annotate
|
| Fri, 11 Mar 2011 08:13:00 +0100 |
bulwahn |
fixing postprocessing; adding a configuration to enable and disable pretty presentation of quickcheck's counterexample
|
file |
diff |
annotate
|
| Fri, 11 Mar 2011 08:12:59 +0100 |
bulwahn |
renaming dest_plain_fun to dest_fun_upds and adding handling of undefined for postprocessing of quickcheck
|
file |
diff |
annotate
|
| Fri, 11 Mar 2011 08:12:58 +0100 |
bulwahn |
improving term postprocessing for counterexample presentation in quickcheck
|
file |
diff |
annotate
|
| Fri, 11 Mar 2011 08:12:55 +0100 |
bulwahn |
tuned
|
file |
diff |
annotate
|
| Mon, 28 Feb 2011 19:06:24 +0100 |
bulwahn |
adding function Quickcheck.test_terms to provide checking a batch of terms
|
file |
diff |
annotate
|
| Mon, 28 Feb 2011 19:06:23 +0100 |
bulwahn |
adding a function to compile a batch of terms for quickcheck with one code generation invocation
|
file |
diff |
annotate
|
| Sat, 08 Jan 2011 17:14:48 +0100 |
wenzelm |
misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
|
file |
diff |
annotate
|
| Wed, 15 Dec 2010 17:46:46 +0100 |
bulwahn |
adding postprocessing for maps in term construction of quickcheck; fixed check_all_option definition
|
file |
diff |
annotate
|
| Wed, 15 Dec 2010 17:46:46 +0100 |
bulwahn |
added enum_term_of to correct present nested functions
|
file |
diff |
annotate
|
| Wed, 15 Dec 2010 17:46:45 +0100 |
bulwahn |
adding postprocessing for sets in term construction of quickcheck
|
file |
diff |
annotate
|
| Wed, 08 Dec 2010 18:07:03 +0100 |
bulwahn |
adding a smarter enumeration scheme for finite functions
|
file |
diff |
annotate
|
| Fri, 03 Dec 2010 08:40:47 +0100 |
bulwahn |
renamed generator into exhaustive
|
file |
diff |
annotate
|
| Fri, 03 Dec 2010 08:40:47 +0100 |
bulwahn |
moving iteration of tests to the testers in quickcheck
|
file |
diff |
annotate
|
| Fri, 03 Dec 2010 08:40:47 +0100 |
bulwahn |
adding smart quantifiers to exhaustive testing
|
file |
diff |
annotate
|
| Fri, 03 Dec 2010 08:40:46 +0100 |
bulwahn |
smallvalue_generator are defined quick via oracle or sound via function package
|
file |
diff |
annotate
|
| Fri, 03 Dec 2010 08:40:46 +0100 |
bulwahn |
improving readability of Smallcheck theory; adding constant orelse to improve performance of the function package
|
file |
diff |
annotate
|
| Wed, 01 Dec 2010 15:35:40 +0100 |
wenzelm |
just one HOLogic.mk_comp;
|
file |
diff |
annotate
|
| Wed, 01 Dec 2010 13:09:08 +0100 |
wenzelm |
just one Term.dest_funT;
|
file |
diff |
annotate
|
| Mon, 22 Nov 2010 10:42:07 +0100 |
bulwahn |
changed old-style quickcheck configurations to new Config.T configurations
|
file |
diff |
annotate
|
| Mon, 22 Nov 2010 10:42:03 +0100 |
bulwahn |
moving the error handling to the right scope in smallvalue_generators
|
file |
diff |
annotate
|
| Mon, 22 Nov 2010 10:42:01 +0100 |
bulwahn |
removing clone from function package and using the clean interface from Function_Relation instead
|
file |
diff |
annotate
|
| Mon, 22 Nov 2010 10:41:58 +0100 |
bulwahn |
adding function generation to SmallCheck; activating exhaustive search space testing
|
file |
diff |
annotate
|
| Mon, 08 Nov 2010 09:25:43 +0100 |
bulwahn |
adding code and theory for smallvalue generators, but do not setup the interpretation yet
|
file |
diff |
annotate
|