| Fri, 17 Jan 2020 16:59:32 +0100 |
wenzelm |
tuned spelling;
|
file |
diff |
annotate
|
| Mon, 03 Jun 2019 15:40:08 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Wed, 06 Dec 2017 20:43:09 +0100 |
wenzelm |
prefer control symbol antiquotations;
|
file |
diff |
annotate
|
| Thu, 14 Apr 2016 15:56:30 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 14 Apr 2016 15:33:51 +0200 |
wenzelm |
misc tuning and standardization;
|
file |
diff |
annotate
|
| Tue, 13 Oct 2015 09:21:15 +0200 |
haftmann |
prod_case as canonical name for product type eliminator
|
file |
diff |
annotate
|
| Tue, 10 Feb 2015 14:48:26 +0100 |
wenzelm |
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
|
file |
diff |
annotate
|
| Fri, 19 Dec 2014 20:10:59 +0100 |
wenzelm |
just one data slot per program unit;
|
file |
diff |
annotate
|
| Fri, 19 Dec 2014 12:56:06 +0100 |
wenzelm |
proper exception for internal program failure, not user-error;
|
file |
diff |
annotate
|
| Wed, 29 Oct 2014 19:01:49 +0100 |
wenzelm |
modernized setup;
|
file |
diff |
annotate
|
| Mon, 13 Oct 2014 18:45:48 +0200 |
wenzelm |
Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings;
|
file |
diff |
annotate
|
| Wed, 17 Sep 2014 08:23:53 +0200 |
blanchet |
support (finite values of) codatatypes in Quickcheck
|
file |
diff |
annotate
|
| Mon, 08 Sep 2014 14:03:57 +0200 |
blanchet |
use compatibility layer
|
file |
diff |
annotate
|
| Fri, 05 Sep 2014 00:41:01 +0200 |
blanchet |
pretend code generation is a ctr_sugar plugin
|
file |
diff |
annotate
|
| Fri, 05 Sep 2014 00:41:01 +0200 |
blanchet |
named interpretations
|
file |
diff |
annotate
|
| Wed, 03 Sep 2014 00:06:17 +0200 |
blanchet |
ported Quickcheck to support new datatypes better
|
file |
diff |
annotate
|
| Mon, 01 Sep 2014 16:17:46 +0200 |
blanchet |
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
|
file |
diff |
annotate
|
| Tue, 19 Aug 2014 09:39:11 +0200 |
blanchet |
reduced dependency on 'Datatype' theory and ML module
|
file |
diff |
annotate
|
| Sat, 22 Mar 2014 21:40:19 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Fri, 21 Mar 2014 11:42:32 +0100 |
wenzelm |
more qualified names;
|
file |
diff |
annotate
|
| Wed, 26 Feb 2014 11:57:52 +0100 |
haftmann |
prefer proof context over background theory
|
file |
diff |
annotate
|
| Tue, 22 Jan 2013 14:33:45 +0100 |
traytel |
separate data used for case translation from the datatype package
|
file |
diff |
annotate
|
| Tue, 22 Jan 2013 13:32:41 +0100 |
berghofe |
case translations performed in a separate check phase (with adjustments by traytel)
|
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
|
| Sun, 11 Nov 2012 19:56:02 +0100 |
haftmann |
dropped dead code;
|
file |
diff |
annotate
|
| Sat, 21 Jul 2012 10:53:26 +0200 |
bulwahn |
handling partiality in the case where the equality optimisation is applied
|
file |
diff |
annotate
|
| Tue, 17 Jul 2012 10:39:39 +0200 |
bulwahn |
improved equality optimisation in Quickcheck
|
file |
diff |
annotate
|
| Mon, 02 Jul 2012 11:45:19 +0200 |
bulwahn |
exporting important function for the "many conjecture refutation" compilation of quickcheck
|
file |
diff |
annotate
|
| Tue, 29 May 2012 13:46:50 +0200 |
bulwahn |
added optimisation for equational premises in Quickcheck; added some Quickcheck examples; NEWS
|
file |
diff |
annotate
|
| Tue, 21 Feb 2012 12:20:33 +0100 |
bulwahn |
subtype preprocessing in Quickcheck;
|
file |
diff |
annotate
|
| Wed, 25 Jan 2012 15:19:04 +0100 |
bulwahn |
generalizing check if size matters because it is different for random and exhaustive testing
|
file |
diff |
annotate
|
| Fri, 20 Jan 2012 09:28:51 +0100 |
bulwahn |
tuned
|
file |
diff |
annotate
|
| Thu, 29 Dec 2011 15:54:37 +0100 |
wenzelm |
comments;
|
file |
diff |
annotate
|
| Tue, 20 Dec 2011 17:22:31 +0100 |
bulwahn |
exporting instantiation functions in quickcheck for their usage in abstract generators
|
file |
diff |
annotate
|
| Tue, 20 Dec 2011 17:22:31 +0100 |
bulwahn |
generalize ensure_sort_datatype to ensure_sort in quickcheck_common to allow generators for abstract types;
|
file |
diff |
annotate
|
| Mon, 05 Dec 2011 12:36:20 +0100 |
bulwahn |
random reporting compilation returns if counterexample is genuine or potentially spurious, and takes genuine_only option as argument
|
file |
diff |
annotate
|
| Mon, 05 Dec 2011 12:36:06 +0100 |
bulwahn |
exhaustive returns if a counterexample is genuine or potentially spurious in the presence of assumptions more correctly
|
file |
diff |
annotate
|
| Mon, 05 Dec 2011 12:35:05 +0100 |
bulwahn |
dynamic genuine_flag in compilation of random and exhaustive
|
file |
diff |
annotate
|
| Mon, 05 Dec 2011 12:35:04 +0100 |
bulwahn |
indicating where the restart should occur; making safe_if dynamic
|
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 |
compilations return genuine flag to quickcheck framework
|
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'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, 30 Nov 2011 09:35:58 +0100 |
bulwahn |
also potential counterexamples in the simple exhaustive testing in quickcheck
|
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
|
| Wed, 30 Nov 2011 09:21:07 +0100 |
bulwahn |
quickcheck returns counterexamples that are potentially spurious due to underspecified code equations and match exceptions
|
file |
diff |
annotate
|
| Mon, 14 Nov 2011 11:14:06 +0100 |
bulwahn |
setting up exhaustive generators which are used for the smart generators
|
file |
diff |
annotate
|
| Wed, 09 Nov 2011 11:35:09 +0100 |
bulwahn |
more precise messages with the tester's name in quickcheck; tuned
|
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
|
| Wed, 17 Aug 2011 18:05:31 +0200 |
wenzelm |
modernized signature of Term.absfree/absdummy;
|
file |
diff |
annotate
|
| Mon, 18 Jul 2011 10:34:21 +0200 |
bulwahn |
changed every tester to have a configuration in quickcheck; enabling parallel testing of different testers in quickcheck
|
file |
diff |
annotate
|
| Mon, 18 Jul 2011 10:34:21 +0200 |
bulwahn |
removing generator registration
|
file |
diff |
annotate
|
| Mon, 18 Jul 2011 10:34:21 +0200 |
bulwahn |
parametrized test_term functions in quickcheck
|
file |
diff |
annotate
|
| Mon, 18 Jul 2011 10:34:21 +0200 |
bulwahn |
adding random, exhaustive and SML quickcheck as testers
|
file |
diff |
annotate
|
| Mon, 02 May 2011 16:33:21 +0200 |
wenzelm |
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
|
file |
diff |
annotate
|
| Mon, 18 Apr 2011 09:10:23 +0200 |
bulwahn |
adding bounded_forall tester
|
file |
diff |
annotate
|
| Mon, 18 Apr 2011 09:10:23 +0200 |
bulwahn |
creating generic test_term function; corrected instantiate_exhaustive_datatype; tuned
|
file |
diff |
annotate
|