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
|
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
|