lemma "k dvd n ==> k dvd (n+1::nat)" nitpick But even with SAT4J I get
Nitpicking~ Nitpick found no counterexample. Of course this is not ideal nitpick country, but still... Tobias Jasmin Christian Blanchette schrieb: > 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 > > _______________________________________________ > Isabelle-dev mailing list > Isabelle-dev at mailbroy.informatik.tu-muenchen.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev