| Tue, 17 Jul 2012 10:39:39 +0200 |
bulwahn |
improved equality optimisation in Quickcheck
|
file |
diff |
annotate
|
| Sat, 17 Mar 2012 09:51:18 +0100 |
wenzelm |
'definition' no longer exports the foundational "raw_def";
|
file |
diff |
annotate
|
| Sat, 17 Mar 2012 00:17:30 +0100 |
wenzelm |
some attempts to fit source on screen;
|
file |
diff |
annotate
|
| Fri, 24 Feb 2012 22:46:44 +0100 |
haftmann |
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
|
file |
diff |
annotate
|
| Fri, 24 Feb 2012 09:40:02 +0100 |
haftmann |
given up disfruitful branch
|
file |
diff |
annotate
|
| Thu, 23 Feb 2012 21:25:59 +0100 |
haftmann |
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
|
file |
diff |
annotate
|
| Mon, 20 Feb 2012 12:37:17 +0100 |
huffman |
use qualified constant names instead of suffixes (from Florian Haftmann)
|
file |
diff |
annotate
|
| Mon, 23 Jan 2012 14:00:52 +0100 |
bulwahn |
random instance for sets
|
file |
diff |
annotate
|
| Fri, 09 Dec 2011 16:08:32 +0100 |
bulwahn |
hiding definitional facts in Quickcheck; introducing catch_match more honestly
|
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:14:35 +0100 |
bulwahn |
making catch_match polymorphic
|
file |
diff |
annotate
|
| Thu, 01 Dec 2011 22:14:35 +0100 |
bulwahn |
quickcheck's compilation returns if it is genuine counterexample or a counterexample due to a match exception
|
file |
diff |
annotate
|
| Thu, 01 Dec 2011 22:14:35 +0100 |
bulwahn |
quickcheck random can also find potential counterexamples;
|
file |
diff |
annotate
|
| Wed, 19 Oct 2011 08:37:24 +0200 |
bulwahn |
removing quickcheck tester SML-inductive based on the old code generator
|
file |
diff |
annotate
|
| Mon, 17 Oct 2011 10:19:01 +0200 |
bulwahn |
moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
|
file |
diff |
annotate
|
| Fri, 09 Sep 2011 00:22:18 +0200 |
krauss |
added syntactic classes for "inf" and "sup"
|
file |
diff |
annotate
|
| Wed, 30 Mar 2011 19:09:56 +0200 |
bulwahn |
removing junk that should not have been committed
|
file |
diff |
annotate
|
| Wed, 30 Mar 2011 11:32:52 +0200 |
bulwahn |
renewing specifications in HOL: replacing types by type_synonym
|
file |
diff |
annotate
|
| 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
|
file |
diff |
annotate
|
| Fri, 11 Mar 2011 15:21:13 +0100 |
bulwahn |
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
|
file |
diff |
annotate
|
| Fri, 11 Mar 2011 15:21:13 +0100 |
bulwahn |
adaptions in generators using the common functions
|
file |
diff |
annotate
|
| Fri, 11 Mar 2011 15:21:13 +0100 |
bulwahn |
renaming signatures and structures; correcting header
|
file |
diff |
annotate
|
| Fri, 11 Mar 2011 15:21:13 +0100 |
bulwahn |
adapting Quickcheck theory after moving ML files
|
file |
diff |
annotate
|
| Mon, 06 Dec 2010 10:52:45 +0100 |
bulwahn |
removing declaration in quickcheck to really enable exhaustive testing
|
file |
diff |
annotate
|
| Fri, 03 Dec 2010 08:40:47 +0100 |
bulwahn |
declaring quickcheck testers as default after their setup
|
file |
diff |
annotate
|
| Mon, 22 Nov 2010 11:34:56 +0100 |
bulwahn |
adding Enum to HOL-Main image and removing it from HOL-Library
|
file |
diff |
annotate
|
| Fri, 27 Aug 2010 19:34:23 +0200 |
haftmann |
renamed class/constant eq to equal; tuned some instantiations
|
file |
diff |
annotate
|
| Fri, 09 Jul 2010 08:11:10 +0200 |
haftmann |
nicer xsymbol syntax for fcomp and scomp
|
file |
diff |
annotate
|
| Fri, 16 Apr 2010 21:28:09 +0200 |
wenzelm |
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
|
file |
diff |
annotate
|
| Wed, 31 Mar 2010 16:44:41 +0200 |
bulwahn |
adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
|
file |
diff |
annotate
|