| Fri, 05 Mar 2021 17:02:32 +0100 |
wenzelm |
tuned --- more elementary Time operations;
|
file |
diff |
annotate
|
| Tue, 29 Sep 2020 11:59:59 +0200 |
wenzelm |
obsolete --- Java is always present via component;
|
file |
diff |
annotate
|
| Tue, 29 Sep 2020 11:35:21 +0200 |
wenzelm |
obsolete --- KODKODI is always present via component;
|
file |
diff |
annotate
|
| Tue, 29 Sep 2020 11:15:51 +0200 |
wenzelm |
obsolete --- ML module Nitpick resides within theory Nitpick (see also 7b8c366e34a2, 1fba360b5443);
|
file |
diff |
annotate
|
| Fri, 25 Sep 2020 15:40:35 +0200 |
wenzelm |
tuned nitpick message: more like quickcheck;
|
file |
diff |
annotate
|
| Tue, 25 Aug 2020 14:54:41 +0200 |
wenzelm |
removed pointless version checks: Isabelle component integration does the job already;
|
file |
diff |
annotate
|
| Sat, 22 Aug 2020 23:11:48 +0200 |
wenzelm |
avoid odd PIDE markup, notably in kokodi input;
|
file |
diff |
annotate
|
| Sat, 05 Jan 2019 17:24:33 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Fri, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Sun, 14 Aug 2016 12:26:09 +0200 |
blanchet |
removed trailing final stops in Nitpick messages
|
file |
diff |
annotate
|
| Sat, 02 Apr 2016 23:29:05 +0200 |
wenzelm |
prefer infix operations;
|
file |
diff |
annotate
|
| Sat, 05 Mar 2016 17:01:45 +0100 |
wenzelm |
tuned signature -- clarified modules;
|
file |
diff |
annotate
|
| Mon, 15 Feb 2016 12:47:52 +0100 |
blanchet |
rephrased message
|
file |
diff |
annotate
|
| Thu, 08 Oct 2015 23:40:27 +0200 |
blanchet |
made TPTP SZS status more compliant
|
file |
diff |
annotate
|
| Fri, 02 Oct 2015 21:24:37 +0200 |
blanchet |
removed Nitpick nonblocking mode, that was never really used
|
file |
diff |
annotate
|
| Fri, 02 Oct 2015 21:06:32 +0200 |
blanchet |
better compliance with TPTP SZS standard
|
file |
diff |
annotate
|
| Sun, 16 Aug 2015 18:19:30 +0200 |
wenzelm |
prefer theory_id operations;
|
file |
diff |
annotate
|
| Fri, 29 May 2015 17:56:43 +0200 |
blanchet |
removed model checks from Nitpick
|
file |
diff |
annotate
|
| Sat, 11 Apr 2015 23:30:30 +0200 |
wenzelm |
proper Pretty.brk -- redundant spaces do not survive Pretty.text (see also 42b7b76b37b8, e06eabc421e7);
|
file |
diff |
annotate
|
| Wed, 08 Apr 2015 19:39:08 +0200 |
wenzelm |
proper context for Object_Logic operations;
|
file |
diff |
annotate
|
| Wed, 04 Mar 2015 19:53:18 +0100 |
wenzelm |
tuned signature -- prefer qualified names;
|
file |
diff |
annotate
|
| Sat, 24 Jan 2015 21:37:31 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 24 Jan 2015 13:54:19 +0100 |
wenzelm |
avoid newline in Pretty.str;
|
file |
diff |
annotate
|
| Tue, 23 Dec 2014 20:46:42 +0100 |
wenzelm |
explicit message channels for "state", "information";
|
file |
diff |
annotate
|
| Fri, 07 Nov 2014 16:36:55 +0100 |
wenzelm |
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
|
file |
diff |
annotate
|
| Mon, 03 Nov 2014 14:31:15 +0100 |
wenzelm |
eliminated obsolete Proof.goal_message -- print outcome more directly;
|
file |
diff |
annotate
|
| Fri, 31 Oct 2014 11:36:41 +0100 |
wenzelm |
discontinued obsolete Output.urgent_message;
|
file |
diff |
annotate
|
| Tue, 19 Aug 2014 09:39:11 +0200 |
blanchet |
reduced dependency on 'Datatype' theory and ML module
|
file |
diff |
annotate
|
| Fri, 21 Mar 2014 20:33:56 +0100 |
wenzelm |
more qualified names;
|
file |
diff |
annotate
|
| Mon, 03 Mar 2014 22:33:22 +0100 |
blanchet |
tuned ML names
|
file |
diff |
annotate
|
| Mon, 03 Mar 2014 22:33:22 +0100 |
blanchet |
tuned code
|
file |
diff |
annotate
|
| Mon, 03 Mar 2014 22:33:22 +0100 |
blanchet |
removed nonstandard models from Nitpick
|
file |
diff |
annotate
|
| Mon, 17 Feb 2014 22:54:38 +0100 |
blanchet |
simplified data structure by reducing the incidence of clumsy indices
|
file |
diff |
annotate
|
| Thu, 19 Dec 2013 13:43:21 +0100 |
blanchet |
made timeouts in Sledgehammer not be 'option's -- simplified lots of code
|
file |
diff |
annotate
|
| Tue, 24 Sep 2013 11:02:42 +0200 |
blanchet |
encode goal digest in spying log (to detect duplicates)
|
file |
diff |
annotate
|
| Mon, 23 Sep 2013 14:53:43 +0200 |
blanchet |
added "spy" option to Nitpick
|
file |
diff |
annotate
|
| Tue, 03 Sep 2013 19:58:00 +0200 |
wenzelm |
cases: formal binding of 'assumes', with position provided via invoke_case;
|
file |
diff |
annotate
|
| Tue, 03 Sep 2013 13:09:15 +0200 |
wenzelm |
cases: more position information and PIDE markup;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Sat, 13 Jul 2013 13:58:13 +0200 |
wenzelm |
gutter icon for information messages;
|
file |
diff |
annotate
|
| Sat, 13 Jul 2013 13:25:42 +0200 |
wenzelm |
more explicit Markup.information for messages produced by "auto" tools;
|
file |
diff |
annotate
|
| Tue, 28 May 2013 18:17:40 +0200 |
blanchet |
no confusing special behavior in debug mode
|
file |
diff |
annotate
|
| Thu, 16 May 2013 13:34:13 +0200 |
blanchet |
tuning -- renamed '_from_' to '_of_' in Sledgehammer
|
file |
diff |
annotate
|
| Fri, 11 Jan 2013 16:30:56 +0100 |
blanchet |
updated messages
|
file |
diff |
annotate
|
| Wed, 12 Dec 2012 11:18:06 +0100 |
blanchet |
got rid of support for Kodkodi < 1.2.14
|
file |
diff |
annotate
|
| Mon, 10 Dec 2012 13:52:33 +0100 |
wenzelm |
generalized notion of active area, where sendback is just one application;
|
file |
diff |
annotate
|
| Mon, 26 Nov 2012 16:16:47 +0100 |
wenzelm |
more general sendback properties;
|
file |
diff |
annotate
|
| Mon, 26 Nov 2012 11:59:56 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 25 Nov 2012 19:49:24 +0100 |
wenzelm |
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
|
file |
diff |
annotate
|
| Thu, 22 Nov 2012 13:21:02 +0100 |
wenzelm |
more abstract Sendback operations, with explicit id/exec_id properties;
|
file |
diff |
annotate
|
| Fri, 14 Sep 2012 18:12:41 +0200 |
wenzelm |
clarified markup names;
|
file |
diff |
annotate
|
| Thu, 30 Aug 2012 09:47:46 +0200 |
blanchet |
updated Java-related error message
|
file |
diff |
annotate
|
| Wed, 18 Jul 2012 08:44:04 +0200 |
blanchet |
optimized MaSh output by chunking it
|
file |
diff |
annotate
|
| Wed, 25 Apr 2012 15:54:36 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Wed, 25 Apr 2012 14:33:21 +0200 |
blanchet |
output SZS status as early as possible
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Tue, 24 Apr 2012 09:47:40 +0200 |
blanchet |
add a timeout on the monotonicity check
|
file |
diff |
annotate
|
| Tue, 24 Apr 2012 09:47:40 +0200 |
blanchet |
handle TPTP definitions as definitions in Nitpick rather than as axioms
|
file |
diff |
annotate
|
| Sun, 22 Apr 2012 14:16:46 +0200 |
blanchet |
added timeout argument to TPTP tools
|
file |
diff |
annotate
|
| Wed, 18 Apr 2012 23:13:10 +0200 |
blanchet |
more standard SZS output
|
file |
diff |
annotate
|