| Thu, 21 Jan 2010 12:18:41 +0100 |
bulwahn |
adopting predicate compiler to new Spec_Rules and eliminating the use of Nitpick_Simps
|
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
|
| Thu, 19 Nov 2009 08:25:57 +0100 |
bulwahn |
replacing Predicate_Compile_Preproc_Const_Defs by more general Spec_Rules
|
file |
diff |
annotate
|
| Thu, 12 Nov 2009 09:10:07 +0100 |
bulwahn |
adding more tests for the values command; adding some forbidden constants to inductify
|
file |
diff |
annotate
|
| Sun, 08 Nov 2009 18:43:42 +0100 |
wenzelm |
adapted Theory_Data;
|
file |
diff |
annotate
|
| Fri, 06 Nov 2009 08:47:32 +0100 |
bulwahn |
merged
|
file |
diff |
annotate
|
| Fri, 06 Nov 2009 08:11:58 +0100 |
bulwahn |
made SML/NJ happy; tuned
|
file |
diff |
annotate
|
| Thu, 05 Nov 2009 16:10:49 +0100 |
wenzelm |
eliminated funny record patterns and made SML/NJ happy;
|
file |
diff |
annotate
|
| Tue, 03 Nov 2009 10:24:06 +0100 |
bulwahn |
adapted the inlining in the predicate compiler
|
file |
diff |
annotate
|
| Sat, 31 Oct 2009 10:02:37 +0100 |
bulwahn |
predicate compiler creates code equations for predicates with full mode
|
file |
diff |
annotate
|
| Wed, 28 Oct 2009 00:07:51 +0100 |
wenzelm |
proper headers;
|
file |
diff |
annotate
|
| Tue, 27 Oct 2009 09:03:56 +0100 |
bulwahn |
print retrieved specification when printing intermediate results
|
file |
diff |
annotate
|
| Tue, 27 Oct 2009 09:02:22 +0100 |
bulwahn |
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
|
file |
diff |
annotate
|