| Mon, 21 Feb 2011 18:28:28 +0100 |
blanchet |
adjust example
|
file |
diff |
annotate
|
| Mon, 21 Feb 2011 10:42:29 +0100 |
blanchet |
always unfold constant defitions marked with "nitpick_def" -- to prevent unfolding, there's already "nitpick_simp"
|
file |
diff |
annotate
|
| Wed, 12 Jan 2011 15:22:24 +0100 |
wenzelm |
compile;
|
file |
diff |
annotate
|
| Wed, 12 Jan 2011 15:08:21 +0100 |
wenzelm |
reraise interrupts as usual;
|
file |
diff |
annotate
|
| Wed, 29 Dec 2010 12:34:33 +0100 |
wenzelm |
made SML/NJ happy;
|
file |
diff |
annotate
|
| Tue, 07 Dec 2010 11:56:56 +0100 |
blanchet |
simplify monotonicity code after killing "fin_fun" optimization
|
file |
diff |
annotate
|
| Mon, 06 Dec 2010 13:33:09 +0100 |
blanchet |
cleanup example
|
file |
diff |
annotate
|
| Mon, 06 Dec 2010 13:33:09 +0100 |
blanchet |
add more flexibility to the monotonicity calculus: instead of hardcoding F-arrows, also allow G-arrows, simulating applications of the Sub rule
|
file |
diff |
annotate
|
| Mon, 06 Dec 2010 13:33:09 +0100 |
blanchet |
improve precision of forall in constancy part of the monotonicity calculus
|
file |
diff |
annotate
|
| Mon, 06 Dec 2010 13:33:09 +0100 |
blanchet |
more work on the monotonicity evaluation driver
|
file |
diff |
annotate
|
| Mon, 06 Dec 2010 13:33:09 +0100 |
blanchet |
added ML code for testing entire theories for monotonicity
|
file |
diff |
annotate
|
| Mon, 06 Dec 2010 13:33:09 +0100 |
blanchet |
added examples to exercise new monotonicity code
|
file |
diff |
annotate
|
| Mon, 06 Dec 2010 13:18:25 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Tue, 14 Sep 2010 13:24:18 +0200 |
blanchet |
remove "fast_descs" option from Nitpick;
|
file |
diff |
annotate
|
| Thu, 05 Aug 2010 21:56:22 +0200 |
blanchet |
added record field
|
file |
diff |
annotate
|
| Mon, 21 Jun 2010 11:16:00 +0200 |
blanchet |
adjusted Nitpick examples to latest changes + make them slightly faster
|
file |
diff |
annotate
|
| Tue, 01 Jun 2010 17:04:21 +0200 |
blanchet |
adapt example
|
file |
diff |
annotate
|
| Sun, 25 Apr 2010 00:10:30 +0200 |
blanchet |
remove "skolemize" option from Nitpick, since Skolemization is always useful
|
file |
diff |
annotate
|
| Wed, 17 Mar 2010 16:26:08 +0100 |
blanchet |
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
|
file |
diff |
annotate
|
| Wed, 17 Mar 2010 09:14:43 +0100 |
blanchet |
added support for "specification" and "ax_specification" constructs to Nitpick
|
file |
diff |
annotate
|
| Fri, 26 Feb 2010 16:49:46 +0100 |
blanchet |
more work on the new monotonicity stuff in Nitpick
|
file |
diff |
annotate
|
| Thu, 25 Feb 2010 16:33:39 +0100 |
blanchet |
improved precision of infinite "shallow" datatypes in Nitpick;
|
file |
diff |
annotate
|
| Wed, 24 Feb 2010 11:07:58 +0100 |
blanchet |
make example compile
|
file |
diff |
annotate
|
| Wed, 17 Feb 2010 20:50:14 +0100 |
blanchet |
fix example to reflect change in function signature
|
file |
diff |
annotate
|
| Fri, 05 Feb 2010 14:27:21 +0100 |
blanchet |
added hotel key card example for Nitpick, and renumber atoms in Nitpick's output for increased readability
|
file |
diff |
annotate
|
| Thu, 04 Feb 2010 16:50:26 +0100 |
blanchet |
adapted example following previous Nitpick change and fixed minor optimization in Nitpick
|
file |
diff |
annotate
|
| Tue, 02 Feb 2010 11:38:38 +0100 |
blanchet |
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
|
file |
diff |
annotate
|
| Thu, 17 Dec 2009 15:22:11 +0100 |
blanchet |
added support for binary nat/int representation to Nitpick
|
file |
diff |
annotate
|
| Sun, 15 Nov 2009 19:44:16 +0100 |
wenzelm |
provide actual Nitpick_HOL.extended_context;
|
file |
diff |
annotate
|
| Thu, 29 Oct 2009 16:06:28 +0100 |
blanchet |
rename "NitpickMono" to "Nitpick_Mono" in example
|
file |
diff |
annotate
|
| Tue, 27 Oct 2009 14:40:24 +0100 |
blanchet |
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
|
file |
diff |
annotate
|
| Fri, 23 Oct 2009 18:59:24 +0200 |
blanchet |
continuation of Nitpick's integration into Isabelle;
|
file |
diff |
annotate
|