src/HOL/Tools/Nitpick/nitpick.ML
Wed, 02 Mar 2011 15:51:22 +0100 blanchet added missing spaces in output
Wed, 02 Mar 2011 14:50:16 +0100 blanchet lower threshold for implicitly using "nitpick_simp" for predicate definitions when "total_consts" is on
Wed, 02 Mar 2011 13:09:57 +0100 blanchet robust handling of types occurring in "eval" and "preconstr" options but not in the goal
Wed, 02 Mar 2011 13:09:57 +0100 blanchet make "preconstr" option more robust -- shouldn't throw exceptions
Mon, 28 Feb 2011 17:53:10 +0100 blanchet if "total_consts" is set, report cex's as quasi-genuine
Mon, 28 Feb 2011 17:53:10 +0100 blanchet added "total_consts" option
Mon, 21 Feb 2011 17:36:32 +0100 blanchet more work on "fix_datatype_vals" optimization (renamed "preconstruct")
Mon, 21 Feb 2011 16:33:21 +0100 blanchet more work on "fix_datatype_vals"
Mon, 21 Feb 2011 15:45:44 +0100 blanchet first steps in implementing "fix_datatype_vals" optimization
Mon, 21 Feb 2011 11:50:31 +0100 blanchet tweaked Nitpick based on C++ memory model example
Mon, 21 Feb 2011 10:42:29 +0100 blanchet always unfold constant defitions marked with "nitpick_def" -- to prevent unfolding, there's already "nitpick_simp"
Mon, 21 Feb 2011 10:29:13 +0100 blanchet don't distinguish between "fixes" and other free variables -- this confuses users
Fri, 18 Feb 2011 16:19:08 +0100 blanchet make Nitpick's timeout mechanism somewhat more reliable/friendly;
Sun, 19 Dec 2010 11:48:42 +0100 blanchet added a timestamp to Nitpick in verbose mode for debugging purposes;
Tue, 07 Dec 2010 11:56:53 +0100 blanchet remove the "fin_fun" optimization in Nitpick -- it was always a hack and didn't help much
less more (0) -100 -15 tip