| Wed, 09 Sep 2015 17:07:44 +0200 |
Andreas Lochbihler |
reactivate examples with predicate compiler and quickcheck
|
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
|
| Fri, 31 Oct 2014 11:36:41 +0100 |
wenzelm |
discontinued obsolete Output.urgent_message;
|
file |
diff |
annotate
|
| Wed, 29 Oct 2014 11:13:24 +0100 |
wenzelm |
modernized setup;
|
file |
diff |
annotate
|
| Sat, 16 Aug 2014 20:46:59 +0200 |
wenzelm |
updated to named_theorems;
|
file |
diff |
annotate
|
| Wed, 26 Feb 2014 11:57:52 +0100 |
haftmann |
prefer proof context over background theory
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 13:33:05 +0100 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Tue, 30 Jul 2013 15:09:25 +0200 |
wenzelm |
type theory is purely value-oriented;
|
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
|
| Thu, 15 Nov 2012 17:40:46 +0100 |
haftmann |
repaired slip accidentally introduced in 57209cfbf16b
|
file |
diff |
annotate
|
| Tue, 13 Nov 2012 09:08:32 +0100 |
haftmann |
prefer explicit Random.seed
|
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
|
| Mon, 14 Nov 2011 11:14:06 +0100 |
bulwahn |
setting up exhaustive generators which are used for the smart generators
|
file |
diff |
annotate
|
| Fri, 11 Nov 2011 12:10:49 +0100 |
bulwahn |
using more conventional names for monad plus operations
|
file |
diff |
annotate
|
| Fri, 11 Nov 2011 08:32:45 +0100 |
bulwahn |
adding CPS compilation to predicate compiler;
|
file |
diff |
annotate
|
| Thu, 20 Oct 2011 09:11:13 +0200 |
bulwahn |
modernizing predicate_compile_quickcheck
|
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 |
adapting quickcheck based on the analysis of the predicate compiler
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 16:15:37 +0200 |
wenzelm |
modernized structure Proof_Context;
|
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
|
| Mon, 21 Mar 2011 08:29:16 +0100 |
bulwahn |
merged
|
file |
diff |
annotate
|
| Fri, 18 Mar 2011 18:19:42 +0100 |
bulwahn |
adapting predicate_compile_quickcheck; tuned
|
file |
diff |
annotate
|
| Sun, 20 Mar 2011 22:08:12 +0100 |
wenzelm |
simplified various cpu_time clones (!): eliminated odd Exn.capture/Exn.release (no need to "stop" timing);
|
file |
diff |
annotate
|
| Sun, 20 Mar 2011 21:28:11 +0100 |
wenzelm |
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
|
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
|
| Fri, 03 Dec 2010 08:40:47 +0100 |
bulwahn |
adapting predicate_compile_quickcheck
|
file |
diff |
annotate
|
| Mon, 25 Oct 2010 21:06:56 +0200 |
wenzelm |
renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
|
file |
diff |
annotate
|
| Fri, 22 Oct 2010 18:38:59 +0200 |
bulwahn |
adding generator quickcheck
|
file |
diff |
annotate
|
| Thu, 21 Oct 2010 19:13:11 +0200 |
bulwahn |
adapting alternative_defs, predicate_compile_quickcheck, examples and code_prolog
|
file |
diff |
annotate
|
| Tue, 28 Sep 2010 12:34:41 +0200 |
krauss |
consolidated tupled_lambda; moved to structure HOLogic
|
file |
diff |
annotate
|
| Mon, 20 Sep 2010 09:26:15 +0200 |
bulwahn |
removing clone in code_prolog and predicate_compile_quickcheck
|
file |
diff |
annotate
|
| Thu, 16 Sep 2010 16:51:33 +0200 |
haftmann |
adjusted to changes in Code_Runtime
|
file |
diff |
annotate
|
| Wed, 15 Sep 2010 15:40:35 +0200 |
haftmann |
Code_Runtime.value, corresponding to ML_Context.value
|
file |
diff |
annotate
|
| Wed, 15 Sep 2010 15:31:32 +0200 |
haftmann |
code_eval renamed to code_runtime
|
file |
diff |
annotate
|
| Wed, 15 Sep 2010 12:16:08 +0200 |
haftmann |
merged
|
file |
diff |
annotate
|
| Wed, 15 Sep 2010 11:30:32 +0200 |
haftmann |
replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references
|
file |
diff |
annotate
|
| Wed, 15 Sep 2010 09:36:39 +0200 |
bulwahn |
adding option show_invalid_clauses for a more detailed message when modes are not inferred
|
file |
diff |
annotate
|
| Wed, 15 Sep 2010 09:36:38 +0200 |
bulwahn |
proposed modes for code_pred now supports modes for mutual predicates
|
file |
diff |
annotate
|
| Thu, 09 Sep 2010 17:23:03 +0200 |
bulwahn |
removing report from the arguments of the quickcheck functions and refering to it by picking it from the context
|
file |
diff |
annotate
|
| Fri, 27 Aug 2010 12:57:55 +0200 |
wenzelm |
merged, resolving some minor conflicts in src/HOL/Tools/Predicate_Compile/code_prolog.ML;
|
file |
diff |
annotate
|
| Thu, 26 Aug 2010 20:51:17 +0200 |
haftmann |
formerly unnamed infix impliciation now named HOL.implies
|
file |
diff |
annotate
|
| Thu, 26 Aug 2010 12:06:00 +0200 |
wenzelm |
standardized Context.copy_thy to Theory.copy alias, with slightly more direct way of using it;
|
file |
diff |
annotate
|
| 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
|