src/HOL/Tools/Nitpick/nitpick.ML
2014-03-21 wenzelm 2014-03-21 more qualified names;
2014-03-03 blanchet 2014-03-03 tuned ML names
2014-03-03 blanchet 2014-03-03 tuned code
2014-03-03 blanchet 2014-03-03 removed nonstandard models from Nitpick
2014-02-17 blanchet 2014-02-17 simplified data structure by reducing the incidence of clumsy indices
2013-12-19 blanchet 2013-12-19 made timeouts in Sledgehammer not be 'option's -- simplified lots of code
2013-09-24 blanchet 2013-09-24 encode goal digest in spying log (to detect duplicates)
2013-09-23 blanchet 2013-09-23 added "spy" option to Nitpick
2013-09-03 wenzelm 2013-09-03 cases: formal binding of 'assumes', with position provided via invoke_case; allow literal equality on type Binding.binding;
2013-09-03 wenzelm 2013-09-03 cases: more position information and PIDE markup;
2013-07-18 wenzelm 2013-07-18 explicit padding on command boundary for "auto" generated sendback -- do not replace the corresponding goal command, but append to it;
2013-07-13 wenzelm 2013-07-13 gutter icon for information messages; avoid redundant Pretty.chunks to keep Markup.information node topmost;
2013-07-13 wenzelm 2013-07-13 more explicit Markup.information for messages produced by "auto" tools;
2013-05-28 blanchet 2013-05-28 no confusing special behavior in debug mode
2013-05-16 blanchet 2013-05-16 tuning -- renamed '_from_' to '_of_' in Sledgehammer
2013-01-11 blanchet 2013-01-11 updated messages
2012-12-12 blanchet 2012-12-12 got rid of support for Kodkodi < 1.2.14
2012-12-10 wenzelm 2012-12-10 generalized notion of active area, where sendback is just one application; some support for graphview via active area;
2012-11-26 wenzelm 2012-11-26 more general sendback properties; support for padding of line boundary, e.g. for ad-hoc insertion of commands via 'help';
2012-11-26 wenzelm 2012-11-26 tuned signature;
2012-11-25 wenzelm 2012-11-25 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
2012-11-22 wenzelm 2012-11-22 more abstract Sendback operations, with explicit id/exec_id properties; purge result messages (again), cf. db58490a68ac, 7b61a539721e;
2012-09-14 wenzelm 2012-09-14 clarified markup names;
2012-08-30 blanchet 2012-08-30 updated Java-related error message
2012-07-18 blanchet 2012-07-18 optimized MaSh output by chunking it
2012-04-25 wenzelm 2012-04-25 merged
2012-04-25 blanchet 2012-04-25 output SZS status as early as possible
2012-04-25 wenzelm 2012-04-25 back to mature jdk1.6.0_31, to avoid issues like Sidekick TAB completion and generic ListCellRenderer;
2012-04-24 blanchet 2012-04-24 add a timeout on the monotonicity check
2012-04-24 blanchet 2012-04-24 handle TPTP definitions as definitions in Nitpick rather than as axioms
2012-04-22 blanchet 2012-04-22 added timeout argument to TPTP tools
2012-04-18 blanchet 2012-04-18 more standard SZS output
2012-04-18 blanchet 2012-04-18 tuned SZS status output
2012-04-18 blanchet 2012-04-18 added SZS status wrappers in TPTP mode
2012-04-18 blanchet 2012-04-18 fixed Auto Nitpick's output
2012-04-16 wenzelm 2012-04-16 more precise handling of java failure, due to missing ISABELLE_JDK_HOME;
2012-03-25 huffman 2012-03-25 merged fork with new numeral representation (see NEWS)
2012-01-17 blanchet 2012-01-17 updated message
2012-01-04 blanchet 2012-01-04 remove subtlety whose justification got lost in time -- the new code is possibly less precise but sounder
2012-01-03 blanchet 2012-01-03 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 blanchet 2012-01-03 rationalized output (a bit)
2011-11-28 wenzelm 2011-11-28 separate module for concrete Isabelle markup;
2011-08-22 blanchet 2011-08-22 more precise warning
2011-06-30 wenzelm 2011-06-30 standardized use of Path operations;
2011-05-27 blanchet 2011-05-27 handle non-auto try case gracefully in Nitpick
2011-05-27 blanchet 2011-05-27 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
2011-05-24 blanchet 2011-05-24 use \<emdash> rather than \<midarrow>
2011-04-27 wenzelm 2011-04-27 direct use of Variable.is_fixed;
2011-04-19 blanchet 2011-04-19 use "Spec_Rules" for finding axioms -- more reliable and cleaner
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-03-18 blanchet 2011-03-18 optimize Kodkod bounds when "need" is specified
2011-03-17 blanchet 2011-03-17 reintroduced "show_skolems" option -- useful when too many Skolems are displayed
2011-03-17 blanchet 2011-03-17 reword Nitpick's wording concerning potential counterexamples
2011-03-15 blanchet 2011-03-15 support non-ground "need" values
2011-03-13 wenzelm 2011-03-13 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 blanchet 2011-03-09 perform no arity check in debug mode so that we get to see the Kodkod problem
2011-03-03 blanchet 2011-03-03 don't forget to look for constants appearing only in "need" option -- otherwise we get exceptions in "the_name" later on
2011-03-03 blanchet 2011-03-03 simplify "need" option's syntax
2011-03-03 blanchet 2011-03-03 renamed "preconstr" option "need"
2011-03-02 blanchet 2011-03-02 added missing spaces in output