| Fri, 11 Nov 2011 10:40:36 +0100 |
bulwahn |
increasing values_timeout to avoid failures of isatest with HOL-IMP
|
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
|
| Sat, 23 Jul 2011 17:22:28 +0200 |
wenzelm |
explicit structure ML_System;
|
file |
diff |
annotate
|
| Tue, 19 Jul 2011 00:07:21 +0200 |
krauss |
values_timeout defaults to 600.0 on SML/NJ -- saves us from cluttering all theories equivalent declarations
|
file |
diff |
annotate
|
| Fri, 01 Jul 2011 15:16:03 +0200 |
wenzelm |
proper @{binding} antiquotations (relevant for formal references);
|
file |
diff |
annotate
|
| Thu, 09 Jun 2011 16:34:49 +0200 |
wenzelm |
discontinued Name.variant to emphasize that this is old-style / indirect;
|
file |
diff |
annotate
|
| Wed, 08 Jun 2011 00:01:20 +0200 |
krauss |
removed generation of instantiated pattern set, which is never actually used
|
file |
diff |
annotate
|
| Wed, 01 Jun 2011 08:07:28 +0200 |
bulwahn |
creating a free variable with proper name and local mixfix syntax (cf. db9b9e46131c)
|
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
|
| Wed, 27 Apr 2011 19:39:50 +0200 |
wenzelm |
some adhoc renaming, to accomodate more strict checks of fixes (cf. 4638622bcaa1);
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 16:15:37 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
| Mon, 28 Mar 2011 10:25:28 +0200 |
bulwahn |
changing values_timeout from a static option to a dynamic option as required for testing with SML/NJ
|
file |
diff |
annotate
|
| Thu, 24 Mar 2011 15:29:31 +0100 |
bulwahn |
allowing special set comprehensions in values command; adding an example for special set comprehension in values
|
file |
diff |
annotate
|
| Wed, 23 Mar 2011 08:50:31 +0100 |
bulwahn |
making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck
|
file |
diff |
annotate
|
| Sun, 20 Mar 2011 21:20:07 +0100 |
wenzelm |
pervasive cond_timeit;
|
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, 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
|
| Tue, 02 Nov 2010 20:55:12 +0100 |
wenzelm |
simplified some time constants;
|
file |
diff |
annotate
|
| Mon, 25 Oct 2010 21:17:14 +0200 |
bulwahn |
renaming split_modeT' to split_modeT
|
file |
diff |
annotate
|
| Mon, 25 Oct 2010 21:17:13 +0200 |
bulwahn |
options as first argument to check functions
|
file |
diff |
annotate
|
| Mon, 25 Oct 2010 21:17:10 +0200 |
bulwahn |
adding a global time limit to the values command
|
file |
diff |
annotate
|
| Fri, 22 Oct 2010 18:38:59 +0200 |
bulwahn |
adding generator quickcheck
|
file |
diff |
annotate
|
| Fri, 22 Oct 2010 18:38:59 +0200 |
bulwahn |
restructuring values command and adding generator compilation
|
file |
diff |
annotate
|
| Thu, 21 Oct 2010 19:13:10 +0200 |
bulwahn |
using a signature in core_data and moving some more functions to core_data
|
file |
diff |
annotate
|
| Thu, 21 Oct 2010 19:13:09 +0200 |
bulwahn |
splitting large core file into core_data, mode_inference and predicate_compile_proof
|
file |
diff |
annotate
|
| Thu, 21 Oct 2010 19:13:09 +0200 |
bulwahn |
added generator_dseq compilation for a sound depth-limited compilation with small value generators
|
file |
diff |
annotate
|
| Thu, 21 Oct 2010 19:13:08 +0200 |
bulwahn |
for now safely but unpractically assume no predicate is terminating
|
file |
diff |
annotate
|