[isabelle-dev] Nitpick counterexample generator now available

[Jasmin Christian Blanchette]

I am pleased to announce the first release of Nitpick, a Kodkod  
(Alloy) based counterexample generator for Isabelle/HOL on which I've  
been working since October. (The name Nitpick is shamelessly stolen  
from an obsolete MIT tool.) The tool is similar to Refute in principle  
but it scales better and produces more genuine counterexamples for  
inductive datatypes.

You can download Nitpick from

http://www4.in.tum.de/~blanchet/nitpick-1.0.0.tgz

It requires a recent snapshot of Isabelle2009. The package contains  
everything you need: Nitpick (.thy + SML), Kodkod (Java), and a SAT  
solver (Java). To install it, just type './build'. The manual is  
included in the package and is also available at

http://www4.in.tum.de/~blanchet/nitpick-1.0.0/Nitpick/Manual/nitpick.pdf

The plan is to release Nitpick 1.1 to the wider public alongside the  
Isabelle2009 "winter" release, and then to incorporate it directly in  
Isabelle from then on.

Please let me know if you have any feedback or bug reports concerning  
Nitpick, or if you find typos in the manual.

Thanks,

Jasmin