src/HOL/Tools/Nitpick/nitpick.ML
2012-11-26 ago more general sendback properties;
2012-11-26 ago tuned signature;
2012-11-25 ago Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
2012-11-22 ago more abstract Sendback operations, with explicit id/exec_id properties;
2012-09-14 ago clarified markup names;
2012-08-30 ago updated Java-related error message
2012-07-18 ago optimized MaSh output by chunking it
2012-04-25 ago merged
2012-04-25 ago output SZS status as early as possible
2012-04-25 ago back to mature jdk1.6.0_31, to avoid issues like Sidekick TAB completion and generic ListCellRenderer;
2012-04-24 ago add a timeout on the monotonicity check
2012-04-24 ago handle TPTP definitions as definitions in Nitpick rather than as axioms
2012-04-22 ago added timeout argument to TPTP tools
2012-04-18 ago more standard SZS output
2012-04-18 ago tuned SZS status output
2012-04-18 ago added SZS status wrappers in TPTP mode
2012-04-18 ago fixed Auto Nitpick's output
2012-04-16 ago more precise handling of java failure, due to missing ISABELLE_JDK_HOME;
2012-03-25 ago merged fork with new numeral representation (see NEWS)
2012-01-17 ago updated message
2012-01-04 ago remove subtlety whose justification got lost in time -- the new code is possibly less precise but sounder
2012-01-03 ago always treat "unit" as a deep datatype, so that we get a good interaction with the record syntax (2.7 of the Nitpick manual)
2012-01-03 ago rationalized output (a bit)
2011-11-28 ago separate module for concrete Isabelle markup;
2011-08-22 ago more precise warning
2011-06-30 ago standardized use of Path operations;
2011-05-27 ago handle non-auto try case gracefully in Nitpick
2011-05-27 ago added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
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