| Tue, 13 Aug 2013 16:25:47 +0200 |
wenzelm |
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
|
file |
diff |
annotate
|
| Sun, 23 Jun 2013 21:16:07 +0200 |
haftmann |
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
|
file |
diff |
annotate
|
| Fri, 15 Feb 2013 08:31:31 +0100 |
haftmann |
two target language numeral types: integer and natural, as replacement for code_numeral;
|
file |
diff |
annotate
|
| Thu, 14 Feb 2013 15:27:10 +0100 |
haftmann |
reform of predicate compiler / quickcheck theories:
|
file |
diff |
annotate
|
| Sat, 20 Oct 2012 09:12:16 +0200 |
haftmann |
moved quite generic material from theory Enum to more appropriate places
|
file |
diff |
annotate
|
| Wed, 22 Aug 2012 22:55:41 +0200 |
wenzelm |
prefer ML_file over old uses;
|
file |
diff |
annotate
|
| Fri, 30 Mar 2012 08:19:29 +0200 |
bulwahn |
hiding fact not so aggressively
|
file |
diff |
annotate
|
| Thu, 15 Mar 2012 22:08:53 +0100 |
wenzelm |
declare command keywords via theory header, including strict checking outside Pure;
|
file |
diff |
annotate
|
| Sun, 05 Feb 2012 08:24:38 +0100 |
bulwahn |
beautifying definitions of check_all and adding instance for finite_4
|
file |
diff |
annotate
|
| Mon, 23 Jan 2012 14:00:52 +0100 |
bulwahn |
random instance for sets
|
file |
diff |
annotate
|
| Fri, 20 Jan 2012 09:28:52 +0100 |
bulwahn |
shortened definitions by adding some termify constants
|
file |
diff |
annotate
|
| Fri, 20 Jan 2012 09:28:50 +0100 |
bulwahn |
adding check_all instance for sets; tuned
|
file |
diff |
annotate
|
| Thu, 12 Jan 2012 10:19:33 +0100 |
bulwahn |
adding exhaustive instances for type constructor set
|
file |
diff |
annotate
|
| Tue, 20 Dec 2011 17:39:56 +0100 |
bulwahn |
quickcheck generators for abstract types; tuned
|
file |
diff |
annotate
|
| Mon, 12 Dec 2011 13:45:54 +0100 |
bulwahn |
hiding constants and facts in the Quickcheck_Exhaustive and Quickcheck_Narrowing theory;
|
file |
diff |
annotate
|
| Sun, 04 Dec 2011 20:05:08 +0100 |
bulwahn |
adding genuine flag to predicate_compile_quickcheck and prolog_quickcheck (cf. 5e46c225370e);
|
file |
diff |
annotate
|
| Thu, 01 Dec 2011 22:16:26 +0100 |
bulwahn |
hiding internal constants and facts more properly
|
file |
diff |
annotate
|
| Thu, 01 Dec 2011 22:16:23 +0100 |
bulwahn |
removing catch_match' now that catch_match is polymorphic
|
file |
diff |
annotate
|
| Thu, 01 Dec 2011 22:14:35 +0100 |
bulwahn |
the simple exhaustive compilation also indicates if counterexample is potentially spurious;
|
file |
diff |
annotate
|
| Thu, 01 Dec 2011 22:14:35 +0100 |
bulwahn |
changing the exhaustive generator signatures;
|
file |
diff |
annotate
|
| Thu, 01 Dec 2011 22:14:35 +0100 |
bulwahn |
quickcheck random can also find potential counterexamples;
|
file |
diff |
annotate
|
| Wed, 30 Nov 2011 15:07:10 +0100 |
bulwahn |
more stable introduction of the internally used unknown term
|
file |
diff |
annotate
|
| Wed, 30 Nov 2011 09:21:09 +0100 |
bulwahn |
adding a exception-safe term reification step in quickcheck; adding examples
|
file |
diff |
annotate
|
| Fri, 11 Nov 2011 08:32:45 +0100 |
bulwahn |
adding CPS compilation to predicate compiler;
|
file |
diff |
annotate
|
| Mon, 18 Jul 2011 10:34:21 +0200 |
bulwahn |
renaming quickcheck_tester to quickcheck_batch_tester; tuned
|
file |
diff |
annotate
|
| Fri, 08 Apr 2011 16:31:14 +0200 |
bulwahn |
splitting exhaustive and full_exhaustive into separate type classes
|
file |
diff |
annotate
|
| Fri, 08 Apr 2011 16:31:14 +0200 |
bulwahn |
theory definitions for fast exhaustive quickcheck compilation
|
file |
diff |
annotate
|
| Fri, 08 Apr 2011 16:31:14 +0200 |
bulwahn |
new compilation for exhaustive quickcheck
|
file |
diff |
annotate
|
| Thu, 07 Apr 2011 14:51:26 +0200 |
bulwahn |
removing instantiation exhaustive for unit in Quickcheck_Exhaustive
|
file |
diff |
annotate
|
| Tue, 05 Apr 2011 09:38:23 +0200 |
bulwahn |
deriving bounded_forall instances in quickcheck_exhaustive
|
file |
diff |
annotate
|
| Fri, 01 Apr 2011 13:49:38 +0200 |
bulwahn |
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
|
file |
diff |
annotate
|
| Fri, 25 Mar 2011 16:03:49 +0100 |
bulwahn |
changing iteration scheme of functions to use minimal number of function updates for exhaustive testing
|
file |
diff |
annotate
|
| Fri, 11 Mar 2011 15:21:13 +0100 |
bulwahn |
moving exhaustive_generators.ML to Quickcheck directory
|
file |
diff |
annotate
|
| Fri, 11 Mar 2011 15:21:13 +0100 |
bulwahn |
replacing naming of small by exhaustive
|
file |
diff |
annotate
|
| Fri, 11 Mar 2011 15:21:13 +0100 |
bulwahn |
renaming constants in Quickcheck_Exhaustive theory
|
file |
diff |
annotate
|
| Fri, 11 Mar 2011 15:21:12 +0100 |
bulwahn |
renaming Smallcheck to Quickcheck_Exhaustive
|
file |
diff |
annotate
| base
|