Hi all, The Nitpick counterexample generator is now [*] part of Isabelle/HOL's repository version. You can use it in any theory that imports Main. Gotcha: You'll need to install Kodkodi (and make sure a Java interpreter is installed).
1. Download http://www4.in.tum.de/~blanchet/kodkodi-1.2.3.tgz 2. Unzip and untar it 3. Put it somewhere you like (e.g., in "/home/nipkow/isabelle/contrib/ kodkodi-1.2.3") 4. Add the path "/home/nipkow/isabelle/contrib/kodkodi-1.2.3" to the bottom of the file "$ISABELLE_HOME/etc/components" Next time you enter a putative lemma, you can type "nitpick" to search for a counterexample. The manual is in "$ISABELLE_HOME/doc-src/ Nitpick"; just do "make pdf" there. I'm currently working on an Auto Nitpick option, just like Auto Quickcheck. Keep syncing. Enjoy! And let me know if you run into problems or have other questions. Jasmin [*] Don't ask for the change set identifier because I couldn't tell you even to save my life. I can tell you that it has been in for the past several hours.
