| Sun, 25 Apr 2010 00:25:44 +0200 |
blanchet |
remove "show_skolems" option and change style of record declarations
|
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
|
| Sat, 24 Apr 2010 17:48:21 +0200 |
blanchet |
removed Nitpick's "uncurry" option
|
file |
diff |
annotate
|
| Sat, 24 Apr 2010 16:43:03 +0200 |
blanchet |
Fruhjahrsputz: remove three mostly useless Nitpick options
|
file |
diff |
annotate
|
| Sat, 24 Apr 2010 16:33:01 +0200 |
blanchet |
remove type annotations as comments;
|
file |
diff |
annotate
|
| Sat, 24 Apr 2010 16:17:30 +0200 |
blanchet |
cosmetics
|
file |
diff |
annotate
|
| Fri, 23 Apr 2010 19:18:39 +0200 |
blanchet |
stop referring to Sledgehammer_Util stuff all over Nitpick code; instead, redeclare any needed function in Nitpick_Util as synonym for the Sledgehammer_Util function of the same name
|
file |
diff |
annotate
|
| Wed, 21 Apr 2010 14:02:19 +0200 |
blanchet |
clarify error message
|
file |
diff |
annotate
|
| Tue, 13 Apr 2010 13:26:06 +0200 |
blanchet |
make Nitpick output everything to tracing in debug mode;
|
file |
diff |
annotate
|
| Tue, 13 Apr 2010 11:43:11 +0200 |
blanchet |
cosmetics
|
file |
diff |
annotate
|
| Wed, 24 Mar 2010 14:43:35 +0100 |
blanchet |
simplify Nitpick parameter parsing code a little bit + make compile
|
file |
diff |
annotate
|
| Wed, 17 Mar 2010 17:23:45 +0100 |
blanchet |
added one-entry cache around Kodkod invocation
|
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
|
| Thu, 11 Mar 2010 12:22:11 +0100 |
blanchet |
added term postprocessor to Nitpick, to provide custom syntax for typedefs
|
file |
diff |
annotate
|
| Wed, 10 Mar 2010 15:06:40 +0100 |
blanchet |
show nice error message in Nitpick when "java" is not available
|
file |
diff |
annotate
|
| Tue, 09 Mar 2010 14:18:21 +0100 |
blanchet |
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
|
file |
diff |
annotate
|
| Tue, 09 Mar 2010 09:25:23 +0100 |
blanchet |
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
|
file |
diff |
annotate
|
| Sat, 27 Feb 2010 23:13:01 +0100 |
wenzelm |
modernized structure Term_Ord;
|
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
|
| Thu, 25 Feb 2010 10:08:44 +0100 |
blanchet |
cosmetics
|
file |
diff |
annotate
|
| Tue, 23 Feb 2010 19:10:25 +0100 |
blanchet |
support local definitions in Nitpick
|
file |
diff |
annotate
|
| Tue, 23 Feb 2010 16:53:13 +0100 |
blanchet |
show Kodkod warning message even in non-verbose mode
|
file |
diff |
annotate
|
| Tue, 23 Feb 2010 15:56:13 +0100 |
blanchet |
distinguish between Kodkodi warnings and errors in Nitpick;
|
file |
diff |
annotate
|
| Mon, 22 Feb 2010 11:57:33 +0100 |
blanchet |
fixed a few bugs in Nitpick and removed unreferenced variables
|
file |
diff |
annotate
|
| Thu, 18 Feb 2010 18:48:07 +0100 |
blanchet |
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
|
file |
diff |
annotate
|
| Wed, 17 Feb 2010 20:46:50 +0100 |
blanchet |
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
|
file |
diff |
annotate
|
| Wed, 17 Feb 2010 12:14:08 +0100 |
blanchet |
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
|
file |
diff |
annotate
|
| Wed, 17 Feb 2010 11:19:48 +0100 |
blanchet |
reintroduce structural induction hint in Nitpick
|
file |
diff |
annotate
|
| Wed, 17 Feb 2010 10:28:04 +0100 |
blanchet |
synchronize Nitpick's wellfoundedness formulas caching
|
file |
diff |
annotate
|
| Fri, 12 Feb 2010 19:44:37 +0100 |
blanchet |
various cosmetic changes to Nitpick
|
file |
diff |
annotate
|
| Fri, 05 Feb 2010 12:04:54 +0100 |
blanchet |
handle Nitpick's nonstandard model enumeration in a cleaner way;
|
file |
diff |
annotate
|
| Thu, 04 Feb 2010 16:03:15 +0100 |
blanchet |
split "nitpick_hol.ML" into two files to make it more manageable;
|
file |
diff |
annotate
|
| Thu, 04 Feb 2010 13:36:52 +0100 |
blanchet |
four changes to 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
|
| Wed, 20 Jan 2010 11:54:19 +0100 |
blanchet |
fix issues with previous Nitpick change
|
file |
diff |
annotate
|
| Wed, 20 Jan 2010 10:38:06 +0100 |
blanchet |
some work on Nitpick's support for quotient types;
|
file |
diff |
annotate
|
| Thu, 14 Jan 2010 17:06:35 +0100 |
blanchet |
removed the Nitpick code that loaded the "Nitpick" theory explicitly if it's not already loaded, because this didn't work properly and is of doubtful value
|
file |
diff |
annotate
|
| Fri, 18 Dec 2009 12:00:29 +0100 |
blanchet |
polished Nitpick's binary integer support etc.;
|
file |
diff |
annotate
|
| Thu, 17 Dec 2009 15:22:11 +0100 |
blanchet |
added support for binary nat/int representation to Nitpick
|
file |
diff |
annotate
|
| Mon, 14 Dec 2009 16:48:49 +0100 |
blanchet |
distinguish better between "complete" (vs. incomplete) types and "concrete" (vs. abstract) types in Nitpick;
|
file |
diff |
annotate
|
| Mon, 14 Dec 2009 12:30:26 +0100 |
blanchet |
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
|
file |
diff |
annotate
|
| Tue, 08 Dec 2009 18:38:08 +0100 |
blanchet |
made Nitpick work also for people who import "Plain" instead of "Main"
|
file |
diff |
annotate
|
| Mon, 07 Dec 2009 13:40:45 +0100 |
blanchet |
make Nitpick output the message "Hint: Maybe you forgot a type constraint?" only for syntactic classes
|
file |
diff |
annotate
|
| Fri, 04 Dec 2009 17:19:59 +0100 |
blanchet |
fixed paths in Nitpick's ML file headers
|
file |
diff |
annotate
|
| Tue, 24 Nov 2009 17:28:25 +0100 |
haftmann |
curried take/drop
|
file |
diff |
annotate
|
| Mon, 23 Nov 2009 18:29:00 +0100 |
blanchet |
fix Nitpick soundness bug related to "finite (UNIV::'a set)" where "'a" is constrained by a sort to be infinite
|
file |
diff |
annotate
|
| Tue, 17 Nov 2009 22:20:51 +0100 |
blanchet |
comment out debugging code in Nitpick
|
file |
diff |
annotate
|
| Tue, 17 Nov 2009 19:47:27 +0100 |
blanchet |
fixed bug in Nitpick's handling of "The" and "Eps" when the return type is a "bool"
|
file |
diff |
annotate
|
| Fri, 13 Nov 2009 15:59:53 +0100 |
blanchet |
removed a few global names in Nitpick (styp, nat_less, pairf)
|
file |
diff |
annotate
|
| Thu, 05 Nov 2009 17:03:22 +0100 |
blanchet |
added datatype constructor cache in Nitpick (to speed up the scope enumeration) and never test more than 4096 scopes
|
file |
diff |
annotate
|
| Thu, 29 Oct 2009 12:50:44 +0100 |
blanchet |
don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)
|
file |
diff |
annotate
|
| Thu, 29 Oct 2009 12:09:32 +0100 |
blanchet |
merged
|
file |
diff |
annotate
|
| Wed, 28 Oct 2009 17:43:43 +0100 |
blanchet |
introduced Auto Nitpick in addition to Auto Quickcheck;
|
file |
diff |
annotate
|
| Tue, 27 Oct 2009 19:00:17 +0100 |
blanchet |
optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
|
file |
diff |
annotate
|
| Tue, 27 Oct 2009 16:52:06 +0100 |
blanchet |
renamed Nitpick option "coalesce_type_vars" to "merge_type_vars" (shorter) and cleaned up old hacks that are no longer necessary
|
file |
diff |
annotate
|
| Wed, 28 Oct 2009 22:18:00 +0100 |
wenzelm |
renamed raw Proof.get_goal to Proof.raw_goal;
|
file |
diff |
annotate
|
| Tue, 27 Oct 2009 15:55:36 +0100 |
blanchet |
added friendly error message when Kodkodi is not available
|
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
|
| Thu, 22 Oct 2009 14:51:47 +0200 |
blanchet |
added Nitpick's theory and ML files to Isabelle/HOL;
|
file |
diff |
annotate
|