Thu, 05 Dec 2013 13:38:20 +0100 |
blanchet |
experiment
|
file |
diff |
annotate
|
Mon, 15 Apr 2013 10:41:03 +0200 |
blanchet |
not all Nitpick 'constructors' are injective -- careful
|
file |
diff |
annotate
|
Fri, 12 Oct 2012 18:58:20 +0200 |
wenzelm |
discontinued obsolete typedef (open) syntax;
|
file |
diff |
annotate
|
Wed, 15 Aug 2012 11:04:56 +0200 |
blanchet |
fixed handling of "int" in the wake of its port to the quotient package
|
file |
diff |
annotate
|
Wed, 30 May 2012 18:09:23 +0200 |
huffman |
temporarily comment out nitpick examples broken by changes to Int.thy
|
file |
diff |
annotate
|
Fri, 11 May 2012 01:02:36 +0200 |
blanchet |
reintroduced example now that it's no longer broken
|
file |
diff |
annotate
|
Thu, 10 May 2012 22:00:24 +0200 |
huffman |
temporarily comment out broken nitpick example;
|
file |
diff |
annotate
|
Tue, 13 Mar 2012 16:56:56 +0100 |
wenzelm |
prefer abs_def over def_raw;
|
file |
diff |
annotate
|
Mon, 20 Feb 2012 12:37:17 +0100 |
huffman |
use qualified constant names instead of suffixes (from Florian Haftmann)
|
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:10 +0100 |
haftmann |
adjusted to set/pred distinction by means of type constructor `set`
|
file |
diff |
annotate
|
Wed, 30 Nov 2011 16:27:10 +0100 |
wenzelm |
prefer typedef without extra definition and alternative name;
|
file |
diff |
annotate
|
Wed, 21 Sep 2011 15:55:16 +0200 |
blanchet |
reintroduced Minipick as Nitpick example
|
file |
diff |
annotate
|
Sat, 20 Aug 2011 09:42:12 +0200 |
haftmann |
deactivated »unknown« nitpick example
|
file |
diff |
annotate
|
Tue, 24 May 2011 00:01:33 +0200 |
blanchet |
use \<emdash> rather than \<midarrow>
|
file |
diff |
annotate
|
Mon, 04 Apr 2011 09:32:50 +0200 |
krauss |
raised timeouts further, for SML/NJ -- because of variations in machines/compilers, fixed timeouts can merely prevent non-termination, not enforce particular performance characteristics.
|
file |
diff |
annotate
|
Fri, 01 Apr 2011 09:48:01 +0200 |
krauss |
raised timeouts further, for SML/NJ
|
file |
diff |
annotate
|
Mon, 28 Mar 2011 17:33:16 +0200 |
krauss |
raised various timeouts to accommodate sluggish SML/NJ
|
file |
diff |
annotate
|
Sun, 19 Dec 2010 11:48:42 +0100 |
blanchet |
added a timestamp to Nitpick in verbose mode for debugging purposes;
|
file |
diff |
annotate
|
Tue, 16 Nov 2010 16:36:57 -0800 |
huffman |
typedef (open) unit
|
file |
diff |
annotate
|
Wed, 03 Nov 2010 22:26:53 +0100 |
blanchet |
standardize on seconds for Nitpick and Sledgehammer timeouts
|
file |
diff |
annotate
|
Tue, 14 Sep 2010 14:22:49 +0200 |
blanchet |
adapt examples to latest Nitpick changes + speed them up a little bit
|
file |
diff |
annotate
|
Wed, 18 Aug 2010 16:59:36 +0200 |
haftmann |
adjusted to restored naming convention of logical record types
|
file |
diff |
annotate
|
Mon, 21 Jun 2010 13:35:10 +0200 |
blanchet |
compile
|
file |
diff |
annotate
|
Mon, 21 Jun 2010 12:28:46 +0200 |
blanchet |
clean up after fcc768dc9dd0
|
file |
diff |
annotate
|
Fri, 11 Jun 2010 17:57:16 +0200 |
blanchet |
adjust Nitpick example to follow latest wave of renamings
|
file |
diff |
annotate
|
Mon, 31 May 2010 18:51:06 +0200 |
blanchet |
obsolete FIXME
|
file |
diff |
annotate
|
Fri, 26 Feb 2010 16:50:09 +0100 |
blanchet |
merged
|
file |
diff |
annotate
|
Fri, 26 Feb 2010 16:49:46 +0100 |
blanchet |
more work on the new monotonicity stuff in Nitpick
|
file |
diff |
annotate
|
Wed, 24 Feb 2010 14:34:40 +0100 |
haftmann |
renamed theory Rational to Rat
|
file |
diff |
annotate
|
Tue, 23 Feb 2010 12:14:29 +0100 |
blanchet |
improved precision of small sets in Nitpick
|
file |
diff |
annotate
|
Mon, 22 Feb 2010 19:31:00 +0100 |
blanchet |
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
|
file |
diff |
annotate
|
Tue, 09 Feb 2010 16:07:51 +0100 |
blanchet |
optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
|
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
|
Fri, 18 Dec 2009 12:00:29 +0100 |
blanchet |
polished Nitpick's binary integer support etc.;
|
file |
diff |
annotate
|
Mon, 14 Dec 2009 10:59:46 +0100 |
blanchet |
make Nitpick tests more robust by specifying SAT solver, singlethreading (in Kodkod, not in Isabelle), and higher time limits
|
file |
diff |
annotate
|
Fri, 04 Dec 2009 17:18:07 +0100 |
blanchet |
make proof work again
|
file |
diff |
annotate
|
Tue, 17 Nov 2009 14:10:31 +0100 |
blanchet |
fixed "expect" of Nitpick examples to reflect latest changes in Nitpick
|
file |
diff |
annotate
|
Thu, 29 Oct 2009 15:24:52 +0100 |
blanchet |
minor cleanup in Nitpick
|
file |
diff |
annotate
|
Fri, 23 Oct 2009 20:13:33 +0200 |
blanchet |
make the Nitpick examples work again
|
file |
diff |
annotate
|
Fri, 23 Oct 2009 18:59:24 +0200 |
blanchet |
continuation of Nitpick's integration into Isabelle;
|
file |
diff |
annotate
|