src/HOL/Tools/Nitpick/nitpick.ML
2016-04-02 ago prefer infix operations;
2016-03-05 ago tuned signature -- clarified modules;
2016-02-15 ago rephrased message
2015-10-08 ago made TPTP SZS status more compliant
2015-10-02 ago removed Nitpick nonblocking mode, that was never really used
2015-10-02 ago better compliance with TPTP SZS standard
2015-08-16 ago prefer theory_id operations;
2015-05-29 ago removed model checks from Nitpick
2015-04-11 ago proper Pretty.brk -- redundant spaces do not survive Pretty.text (see also 42b7b76b37b8, e06eabc421e7);
2015-04-08 ago proper context for Object_Logic operations;
2015-03-04 ago tuned signature -- prefer qualified names;
2015-01-24 ago tuned;
2015-01-24 ago avoid newline in Pretty.str;
2014-12-23 ago explicit message channels for "state", "information";
2014-11-07 ago plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
2014-11-03 ago eliminated obsolete Proof.goal_message -- print outcome more directly;
2014-10-31 ago discontinued obsolete Output.urgent_message;
2014-08-19 ago reduced dependency on 'Datatype' theory and ML module
2014-03-21 ago more qualified names;
2014-03-03 ago tuned ML names
2014-03-03 ago tuned code
2014-03-03 ago removed nonstandard models from Nitpick
2014-02-17 ago simplified data structure by reducing the incidence of clumsy indices
2013-12-19 ago made timeouts in Sledgehammer not be 'option's -- simplified lots of code
2013-09-24 ago encode goal digest in spying log (to detect duplicates)
2013-09-23 ago added "spy" option to Nitpick
2013-09-03 ago cases: formal binding of 'assumes', with position provided via invoke_case;
2013-09-03 ago cases: more position information and PIDE markup;
2013-07-18 ago explicit padding on command boundary for "auto" generated sendback -- do not replace the corresponding goal command, but append to it;
2013-07-13 ago gutter icon for information messages;
2013-07-13 ago more explicit Markup.information for messages produced by "auto" tools;
2013-05-28 ago no confusing special behavior in debug mode
2013-05-16 ago tuning -- renamed '_from_' to '_of_' in Sledgehammer
2013-01-11 ago updated messages
2012-12-12 ago got rid of support for Kodkodi < 1.2.14
2012-12-10 ago generalized notion of active area, where sendback is just one application;
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;