| Mon, 25 Feb 2013 12:17:50 +0100 |
wenzelm |
prefer stateless 'ML_val' for tests;
|
file |
diff |
annotate
|
| Mon, 27 Feb 2012 16:56:25 +0100 |
wenzelm |
more explicit Long_Name operations (NB: analyzing qualifiers is inherently fragile);
|
file |
diff |
annotate
|
| Tue, 03 Jan 2012 18:33:17 +0100 |
blanchet |
reintroduced failing examples now that they work again, after reintroduction of "set"
|
file |
diff |
annotate
|
| Sat, 24 Dec 2011 15:53:11 +0100 |
haftmann |
commented out examples which choke on strict set/pred distinction
|
file |
diff |
annotate
|
| Thu, 01 Dec 2011 13:34:12 +0100 |
blanchet |
minor example tweak
|
file |
diff |
annotate
|
| Wed, 21 Sep 2011 15:55:16 +0200 |
blanchet |
reintroduced Minipick as Nitpick example
|
file |
diff |
annotate
|
| Tue, 19 Apr 2011 14:04:58 +0200 |
blanchet |
use "Spec_Rules" for finding axioms -- more reliable and cleaner
|
file |
diff |
annotate
|
| Thu, 03 Mar 2011 11:20:48 +0100 |
blanchet |
simplify "need" option's syntax
|
file |
diff |
annotate
|
| Thu, 03 Mar 2011 11:20:48 +0100 |
blanchet |
renamed "preconstr" option "need"
|
file |
diff |
annotate
|
| Wed, 02 Mar 2011 14:50:16 +0100 |
blanchet |
lower threshold for implicitly using "nitpick_simp" for predicate definitions when "total_consts" is on
|
file |
diff |
annotate
|
| 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
|