src/HOL/Tools/Nitpick/nitpick.ML
2011-02-21 ago more work on "fix_datatype_vals" optimization (renamed "preconstruct")
2011-02-21 ago more work on "fix_datatype_vals"
2011-02-21 ago first steps in implementing "fix_datatype_vals" optimization
2011-02-21 ago tweaked Nitpick based on C++ memory model example
2011-02-21 ago always unfold constant defitions marked with "nitpick_def" -- to prevent unfolding, there's already "nitpick_simp"
2011-02-21 ago don't distinguish between "fixes" and other free variables -- this confuses users
2011-02-18 ago make Nitpick's timeout mechanism somewhat more reliable/friendly;
2010-12-19 ago added a timestamp to Nitpick in verbose mode for debugging purposes;
2010-12-07 ago remove the "fin_fun" optimization in Nitpick -- it was always a hack and didn't help much
2010-12-07 ago give the inner timeout mechanism a chance, since it gives more precise information to the user
2010-12-07 ago added a hint when the user obviously just forgot a colon after the lemma's name
2010-12-06 ago use ML SAT solvers up to a certain time limit, then switch to faster solvers with a timeout -- this becomes necessary with the new, more powerful monotonicity calculus
2010-12-06 ago removed old baggage from monotonicity calculus -- the "calculus" option didn't really work anyway because of on-the-fly simplifications
2010-12-06 ago support 3 monotonicity calculi in one and fix soundness bug
2010-11-07 ago removed explicit "Interrupt" handling for conformity with async model -- unfortunately the user loses the information about how many scopes were checked, but this needs to be retought with the new interface anyway
2010-11-05 ago explicit indication of some remaining violations of the Isabelle/ML interrupt model;
2010-11-03 ago standardize on seconds for Nitpick and Sledgehammer timeouts
2010-10-28 ago clear identification
2010-10-25 ago renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
2010-09-14 ago tuning
2010-09-14 ago remove "fast_descs" option from Nitpick;
2010-09-13 ago remove unreferenced identifiers
2010-09-11 ago change defaults of Auto Nitpick so that it consumes less resources (time and Kodkod threads)
2010-08-27 ago renamed class/constant eq to equal; tuned some instantiations
2010-08-18 ago with Kodkodi 1.2.15, Java 1.5 is fine
2010-08-18 ago gracefully handle the case where the JVM is too old in Nitpick
2010-08-06 ago local versions of Nitpick.register_xxx functions
2010-08-06 ago added a friendly warning
2010-08-06 ago improved "merge_type_vars" option: map supersorts to subsorts, to avoid distinguishing, say, "{}", and "HOL.type"
2010-08-05 ago added "whack"
2010-08-03 ago better "Pretty" handling
2010-08-03 ago more helpful message
2010-08-03 ago fix soundness bug w.r.t. "Suc" with "binary_ints"
2010-08-03 ago handle free variables even more gracefully;
2010-08-03 ago optimize local "def"s by treating them as definitions
2010-08-01 ago added manual symmetry breaking for datatypes
2010-07-31 ago started implementation of custom sym break
2010-07-31 ago clarify Nitpick's output in case of a potential counterexample
2010-07-21 ago do a better job at Skolemizing in Nitpick, for TPTP FOF
2010-07-03 ago adapt Nitpick to "prod_case" and "*" -> "sum" renaming;
2010-06-22 ago distinguish between "unknown" and "no Kodkodi installed" errors
2010-06-01 ago merged
2010-06-01 ago added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
2010-06-01 ago remove comment
2010-06-01 ago thread along context instead of theory for typedef lookup
2010-05-31 ago modernized some structure names, keeping a few legacy aliases;
2010-05-31 ago fix handling of "split" w.r.t. new definition + fix exception handling w.r.t. "expect" option
2010-05-27 ago renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;
2010-05-14 ago improve precision of set constructs in Nitpick
2010-04-26 ago fixes 2a5c6e7b55cb;
2010-04-26 ago remove needless code that was copy-pasted from Quickcheck (where it made sense)
2010-04-25 ago remove "show_skolems" option and change style of record declarations
2010-04-25 ago remove "skolemize" option from Nitpick, since Skolemization is always useful
2010-04-24 ago removed Nitpick's "uncurry" option
2010-04-24 ago Fruhjahrsputz: remove three mostly useless Nitpick options
2010-04-24 ago remove type annotations as comments;
2010-04-24 ago cosmetics
2010-04-23 ago stop referring to Sledgehammer_Util stuff all over Nitpick code; instead, redeclare any needed function in Nitpick_Util as synonym for the Sledgehammer_Util function of the same name
2010-04-21 ago clarify error message
2010-04-13 ago make Nitpick output everything to tracing in debug mode;