src/HOL/Tools/Nitpick/nitpick.ML
2011-05-24 ago use \<emdash> rather than \<midarrow>
2011-04-27 ago direct use of Variable.is_fixed;
2011-04-19 ago use "Spec_Rules" for finding axioms -- more reliable and cleaner
2011-04-16 ago modernized structure Proof_Context;
2011-03-18 ago optimize Kodkod bounds when "need" is specified
2011-03-17 ago reintroduced "show_skolems" option -- useful when too many Skolems are displayed
2011-03-17 ago reword Nitpick's wording concerning potential counterexamples
2011-03-15 ago support non-ground "need" values
2011-03-13 ago Path.print is the official way to show file-system paths to users -- note that Path.implode often indicates violation of the abstract datatype;
2011-03-09 ago perform no arity check in debug mode so that we get to see the Kodkod problem
2011-03-03 ago don't forget to look for constants appearing only in "need" option -- otherwise we get exceptions in "the_name" later on
2011-03-03 ago simplify "need" option's syntax
2011-03-03 ago renamed "preconstr" option "need"
2011-03-02 ago added missing spaces in output
2011-03-02 ago lower threshold for implicitly using "nitpick_simp" for predicate definitions when "total_consts" is on
2011-03-02 ago robust handling of types occurring in "eval" and "preconstr" options but not in the goal
2011-03-02 ago make "preconstr" option more robust -- shouldn't throw exceptions
2011-02-28 ago if "total_consts" is set, report cex's as quasi-genuine
2011-02-28 ago added "total_consts" option
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