src/HOL/Tools/Nitpick/nitpick.ML
Tue, 24 Sep 2013 11:02:42 +0200 blanchet encode goal digest in spying log (to detect duplicates)
Mon, 23 Sep 2013 14:53:43 +0200 blanchet added "spy" option to Nitpick
Tue, 03 Sep 2013 19:58:00 +0200 wenzelm cases: formal binding of 'assumes', with position provided via invoke_case;
Tue, 03 Sep 2013 13:09:15 +0200 wenzelm cases: more position information and PIDE markup;
Thu, 18 Jul 2013 20:53:22 +0200 wenzelm explicit padding on command boundary for "auto" generated sendback -- do not replace the corresponding goal command, but append to it;
Sat, 13 Jul 2013 13:58:13 +0200 wenzelm gutter icon for information messages;
Sat, 13 Jul 2013 13:25:42 +0200 wenzelm more explicit Markup.information for messages produced by "auto" tools;
Tue, 28 May 2013 18:17:40 +0200 blanchet no confusing special behavior in debug mode
Thu, 16 May 2013 13:34:13 +0200 blanchet tuning -- renamed '_from_' to '_of_' in Sledgehammer
Fri, 11 Jan 2013 16:30:56 +0100 blanchet updated messages
Wed, 12 Dec 2012 11:18:06 +0100 blanchet got rid of support for Kodkodi < 1.2.14
Mon, 10 Dec 2012 13:52:33 +0100 wenzelm generalized notion of active area, where sendback is just one application;
Mon, 26 Nov 2012 16:16:47 +0100 wenzelm more general sendback properties;
Mon, 26 Nov 2012 11:59:56 +0100 wenzelm tuned signature;
Sun, 25 Nov 2012 19:49:24 +0100 wenzelm Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
Thu, 22 Nov 2012 13:21:02 +0100 wenzelm more abstract Sendback operations, with explicit id/exec_id properties;
Fri, 14 Sep 2012 18:12:41 +0200 wenzelm clarified markup names;
Thu, 30 Aug 2012 09:47:46 +0200 blanchet updated Java-related error message
Wed, 18 Jul 2012 08:44:04 +0200 blanchet optimized MaSh output by chunking it
Wed, 25 Apr 2012 15:54:36 +0200 wenzelm merged
Wed, 25 Apr 2012 14:33:21 +0200 blanchet output SZS status as early as possible
Wed, 25 Apr 2012 14:24:27 +0200 wenzelm back to mature jdk1.6.0_31, to avoid issues like Sidekick TAB completion and generic ListCellRenderer;
Tue, 24 Apr 2012 09:47:40 +0200 blanchet add a timeout on the monotonicity check
Tue, 24 Apr 2012 09:47:40 +0200 blanchet handle TPTP definitions as definitions in Nitpick rather than as axioms
Sun, 22 Apr 2012 14:16:46 +0200 blanchet added timeout argument to TPTP tools
Wed, 18 Apr 2012 23:13:10 +0200 blanchet more standard SZS output
Wed, 18 Apr 2012 22:40:25 +0200 blanchet tuned SZS status output
Wed, 18 Apr 2012 22:40:25 +0200 blanchet added SZS status wrappers in TPTP mode
Wed, 18 Apr 2012 22:40:25 +0200 blanchet fixed Auto Nitpick's output
Mon, 16 Apr 2012 15:09:47 +0200 wenzelm more precise handling of java failure, due to missing ISABELLE_JDK_HOME;
less more (0) -100 -50 -30 tip