2010-03-19 blanchet 2010-03-19 move the Sledgehammer Isar commands together into one file; this will make easier to add options and reorganize them later
2010-03-09 blanchet 2010-03-09 added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
2010-02-22 blanchet 2010-02-22 fixed a few bugs in Nitpick and removed unreferenced variables
2010-02-02 blanchet 2010-02-02 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
2010-01-20 blanchet 2010-01-20 some work on Nitpick's support for quotient types; quotient types are not yet in Isabelle, so for now I hardcoded "IntEx.my_int"
2009-12-17 blanchet 2009-12-17 added support for binary nat/int representation to Nitpick
2009-12-14 blanchet 2009-12-14 get rid of polymorphic equality in Nitpick's code + a few minor cleanups
2009-12-04 blanchet 2009-12-04 fixed paths in Nitpick's ML file headers
2009-11-15 wenzelm 2009-11-15 permissive AList.merge -- most likely setup for theory data (beware of spurious AList.DUP);
2009-11-10 wenzelm 2009-11-10 Toplevel.thread provides Isar-style exception output;
2009-11-10 wenzelm 2009-11-10 plain add_preference, no setmp_CRITICAL required;
2009-11-10 wenzelm 2009-11-10 recovered update from 7264824baf66, which got lost in 7264824baf66;
2009-11-10 blanchet 2009-11-10 remove spurious parameter to "merge"
2009-11-10 blanchet 2009-11-10 merged, and renamed local "TheoryData" to "Data" (following common Isabelle conventions)
2009-10-29 blanchet 2009-10-29 merged
2009-10-28 blanchet 2009-10-28 introduced Auto Nitpick in addition to Auto Quickcheck; this required generalizing the theorem hook used by Quickcheck, following a suggestion by Florian
2009-10-27 blanchet 2009-10-27 renamed Nitpick option "coalesce_type_vars" to "merge_type_vars" (shorter) and cleaned up old hacks that are no longer necessary
2009-11-08 wenzelm 2009-11-08 adapted Theory_Data; tuned;
2009-10-28 wenzelm 2009-10-28 renamed raw Proof.get_goal to Proof.raw_goal;
2009-10-27 blanchet 2009-10-27 internal renaming in Nitpick and fixed Kodkodi invokation on Linux; renamed Nitpick's ML structures from NitpickXxx to Nitpick_Xxx and added KODKODI_JAVA_LIBRARY_PATH to LD_LIBRARY_PATH before invoking Kodkodi
2009-10-27 wenzelm 2009-10-27 SimpleThread.fork: uniform handling of outermost Interrupt, which is not an error and should not produce exception trace;
2009-10-23 blanchet 2009-10-23 continuation of Nitpick's integration into Isabelle; added examples, and integrated non-Main theories better.
2009-10-22 blanchet 2009-10-22 added Nitpick's theory and ML files to Isabelle/HOL; the examples and the documentation are on their way.