Wed, 15 Sep 2010 15:31:32 +0200 |
haftmann |
code_eval renamed to code_runtime
|
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
|
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
|
Thu, 09 Sep 2010 16:43:57 +0200 |
bulwahn |
changing the container for the quickcheck options to a generic data
|
file |
diff |
annotate
|
Thu, 26 Aug 2010 20:51:17 +0200 |
haftmann |
formerly unnamed infix impliciation now named HOL.implies
|
file |
diff |
annotate
|
Thu, 19 Aug 2010 12:11:57 +0200 |
haftmann |
use HOLogic.boolT and @{typ bool} more pervasively
|
file |
diff |
annotate
|
Thu, 19 Aug 2010 11:02:14 +0200 |
haftmann |
use antiquotations for remaining unqualified constants in HOL
|
file |
diff |
annotate
|
Wed, 18 Aug 2010 16:59:37 +0200 |
haftmann |
tuned signature and code
|
file |
diff |
annotate
|
Thu, 12 Aug 2010 17:56:41 +0200 |
haftmann |
group record-related ML files
|
file |
diff |
annotate
|
Wed, 11 Aug 2010 14:31:43 +0200 |
haftmann |
moved instantiation target formally to class_target.ML
|
file |
diff |
annotate
|
Thu, 08 Jul 2010 16:19:24 +0200 |
haftmann |
tuned titles
|
file |
diff |
annotate
|
Mon, 28 Jun 2010 15:03:07 +0200 |
haftmann |
merged constants "split" and "prod_case"
|
file |
diff |
annotate
|
Wed, 26 May 2010 16:05:25 +0200 |
haftmann |
dropped legacy theorem bindings
|
file |
diff |
annotate
|
Sat, 20 Mar 2010 17:33:11 +0100 |
wenzelm |
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
|
file |
diff |
annotate
|
Thu, 25 Feb 2010 09:28:01 +0100 |
bulwahn |
added basic reporting of test cases to quickcheck
|
file |
diff |
annotate
|
Wed, 17 Feb 2010 13:48:13 +0100 |
haftmann |
tuned primrec signature: return definienda
|
file |
diff |
annotate
|
Wed, 27 Jan 2010 14:02:52 +0100 |
haftmann |
corrected type of typecopy constructor
|
file |
diff |
annotate
|
Mon, 07 Dec 2009 16:27:48 +0100 |
haftmann |
split off evaluation mechanisms in separte module Code_Eval
|
file |
diff |
annotate
|
Mon, 30 Nov 2009 11:42:49 +0100 |
haftmann |
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
|
file |
diff |
annotate
|
Thu, 19 Nov 2009 14:46:33 +0100 |
wenzelm |
adapted Local_Theory.define -- eliminated odd thm kind;
|
file |
diff |
annotate
|
Fri, 13 Nov 2009 21:11:15 +0100 |
wenzelm |
modernized structure Local_Theory;
|
file |
diff |
annotate
|
Fri, 13 Nov 2009 20:41:29 +0100 |
wenzelm |
eliminated slightly odd kind argument of LocalTheory.note(s);
|
file |
diff |
annotate
|
Fri, 13 Nov 2009 17:25:09 +0100 |
wenzelm |
eliminated obsolete "generated" kind -- collapsed to unspecific "" (definitely unused according to Lukas Bulwahn);
|
file |
diff |
annotate
|
Tue, 10 Nov 2009 16:04:57 +0100 |
wenzelm |
modernized structure Theory_Target;
|
file |
diff |
annotate
|
Tue, 10 Nov 2009 15:33:35 +0100 |
wenzelm |
removed unused Quickcheck_RecFun_Simps;
|
file |
diff |
annotate
|
Wed, 28 Oct 2009 16:28:12 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Tue, 27 Oct 2009 17:34:00 +0100 |
wenzelm |
normalized basic type abbreviations;
|
file |
diff |
annotate
|
Mon, 26 Oct 2009 15:15:59 +0100 |
haftmann |
conceal quickcheck generators
|
file |
diff |
annotate
|
Sat, 24 Oct 2009 17:47:53 +0200 |
wenzelm |
handle Sorts.CLASS_ERROR instead of arbitrary exceptions;
|
file |
diff |
annotate
|
Wed, 21 Oct 2009 17:34:35 +0200 |
blanchet |
renamed "nitpick_const_xxx" attributes to "nitpick_xxx" and "nitpick_ind_intros" to "nitpick_intros"
|
file |
diff |
annotate
|
Tue, 20 Oct 2009 20:54:31 +0200 |
wenzelm |
uniform use of Integer.min/max;
|
file |
diff |
annotate
|
Sat, 17 Oct 2009 16:58:03 +0200 |
wenzelm |
operations of structure Skip_Proof (formerly SkipProof) no longer require quick_and_dirty mode;
|
file |
diff |
annotate
|
Tue, 29 Sep 2009 16:24:36 +0200 |
wenzelm |
explicit indication of Unsynchronized.ref;
|
file |
diff |
annotate
|
Wed, 23 Sep 2009 14:00:12 +0200 |
haftmann |
Code_Eval(uation)
|
file |
diff |
annotate
|
Sat, 15 Aug 2009 15:29:53 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
Thu, 30 Jul 2009 15:21:31 +0200 |
haftmann |
more appropriate printing of function terms
|
file |
diff |
annotate
|
Fri, 10 Jul 2009 07:59:23 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
Mon, 06 Jul 2009 16:49:51 +0200 |
haftmann |
tuned code
|
file |
diff |
annotate
|
Fri, 03 Jul 2009 16:51:06 +0200 |
haftmann |
proper closures -- imperative programming considered harmful...
|
file |
diff |
annotate
|
Thu, 02 Jul 2009 17:34:14 +0200 |
wenzelm |
renamed NamedThmsFun to Named_Thms;
|
file |
diff |
annotate
|
Mon, 29 Jun 2009 16:17:56 +0200 |
haftmann |
canonical prefix for datatype derivates
|
file |
diff |
annotate
|
Tue, 23 Jun 2009 17:17:07 +0200 |
haftmann |
tuned proof
|
file |
diff |
annotate
|
Tue, 23 Jun 2009 16:27:12 +0200 |
haftmann |
tuned interfaces of datatype module
|
file |
diff |
annotate
|
Sun, 21 Jun 2009 21:37:24 +0200 |
haftmann |
more precise computation of sort constraints
|
file |
diff |
annotate
|
Sun, 21 Jun 2009 08:38:58 +0200 |
haftmann |
simplified names of common datatype types
|
file |
diff |
annotate
|
Fri, 19 Jun 2009 17:23:21 +0200 |
haftmann |
discontinued ancient tradition to suffix certain ML module names with "_package"
|
file |
diff |
annotate
|
Wed, 17 Jun 2009 08:31:13 +0200 |
haftmann |
merged
|
file |
diff |
annotate
|
Tue, 16 Jun 2009 16:37:07 +0200 |
haftmann |
datatype packages: record datatype_config for configuration flags; less verbose signatures
|
file |
diff |
annotate
|
Mon, 15 Jun 2009 21:33:27 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
Mon, 15 Jun 2009 17:36:49 +0200 |
wenzelm |
made SML/NJ happy;
|
file |
diff |
annotate
|
Mon, 15 Jun 2009 16:13:03 +0200 |
haftmann |
hide constant Quickcheck.random
|
file |
diff |
annotate
|
Sun, 14 Jun 2009 09:13:06 +0200 |
haftmann |
dropped diagnostic handles
|
file |
diff |
annotate
|
Sat, 13 Jun 2009 10:01:01 +0200 |
haftmann |
using SkipProof where appropriate
|
file |
diff |
annotate
|
Sat, 13 Jun 2009 09:16:25 +0200 |
haftmann |
quickcheck generators for datatypes with functions
|
file |
diff |
annotate
|
Thu, 11 Jun 2009 08:02:27 +0200 |
haftmann |
explicit instantiation yields considerable speedup
|
file |
diff |
annotate
|
Wed, 10 Jun 2009 16:22:54 +0200 |
haftmann |
tuned whitespace
|
file |
diff |
annotate
|
Wed, 10 Jun 2009 16:10:31 +0200 |
haftmann |
correct check for instantiatability
|
file |
diff |
annotate
|
Wed, 10 Jun 2009 15:04:32 +0200 |
haftmann |
revised interpretation combinator for datatype constructions
|
file |
diff |
annotate
|
Tue, 09 Jun 2009 22:59:54 +0200 |
haftmann |
first running version of qc generators for datatypes
|
file |
diff |
annotate
|
Mon, 08 Jun 2009 08:38:53 +0200 |
haftmann |
added infrastructure for definitorial construction of generators for datatypes
|
file |
diff |
annotate
|