Tue, 28 Sep 2021 17:08:38 +0200 wenzelm more convenient ML arguments: avoid excessive nesting of cartouches;
Tue, 28 Sep 2021 16:01:13 +0200 wenzelm outer syntax: support for control-cartouche tokens;
Tue, 28 Sep 2021 20:58:04 +0200 nipkow merged
Tue, 28 Sep 2021 20:57:57 +0200 nipkow An example
Wed, 29 Sep 2021 09:34:15 +0200 Fabian Huch tuned; draft
Tue, 28 Sep 2021 13:55:39 +0200 Fabian Huch test-tuned; draft
Tue, 28 Sep 2021 11:30:14 +0200 Fabian Huch merged draft
Fri, 10 Sep 2021 21:02:49 +0200 Fabian Huch tuned;
Wed, 08 Sep 2021 16:53:16 +0200 Fabian Huch vscode improvements: overhauled
Fri, 03 Sep 2021 15:03:29 +0200 Fabian Huch vscode improvements: initial
Tue, 28 Sep 2021 12:28:55 +0200 desharna updated Sledgehammer to support zipperposition 2.1 draft
Tue, 28 Sep 2021 11:11:44 +0200 desharna fixed veriT environment variable in sledgehammer's documentation draft
Tue, 28 Sep 2021 10:47:18 +0200 desharna prefer veriT over Z3 in sledgehammer
Tue, 28 Sep 2021 10:38:36 +0200 desharna added Zipperposition to sledgehammer's default provers
Mon, 27 Sep 2021 20:45:26 +0200 wenzelm provide zipperposition-2.1 (still unused);
Mon, 27 Sep 2021 12:39:02 +0200 Lukas Stevens Fix eta-contraction issue, improve tracing draft
Mon, 27 Sep 2021 12:33:28 +0200 Lukas Stevens merged; draft order-prover
Mon, 27 Sep 2021 11:19:56 +0200 blanchet tuned docs
Sun, 26 Sep 2021 20:13:28 +0200 wenzelm merged
Sun, 26 Sep 2021 18:49:55 +0200 wenzelm improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
Sat, 25 Sep 2021 07:45:27 +0000 haftmann NOT is part of syntax bundle also
Fri, 24 Sep 2021 22:44:13 +0200 wenzelm merged
Fri, 24 Sep 2021 22:23:26 +0200 wenzelm tuned proofs --- avoid 'guess';
Fri, 24 Sep 2021 11:04:18 +0000 haftmann apply declarations from interpretations in eigen context also
Fri, 24 Sep 2021 13:40:14 +0200 wenzelm grant access to sun.tools.jconsole, as required for Java 17;
Fri, 24 Sep 2021 12:53:11 +0200 wenzelm update to e-2.6, following Martin Desharnais;
Mon, 27 Sep 2021 10:32:21 +0000 Lukas Stevens Fix eta-contraction issues and add proper tracing draft order-prover
Thu, 23 Sep 2021 18:18:36 +0200 Lukas Stevens Don't recurse more than one level for Not draft closure-solver
Thu, 23 Sep 2021 16:17:59 +0000 Lukas Stevens Begin debugging failure in HOL-Analysis draft order-prover
Thu, 23 Sep 2021 14:55:40 +0200 Lukas Stevens merged; draft order-prover
Thu, 23 Sep 2021 14:42:15 +0200 Lukas Stevens merged; draft
Thu, 23 Sep 2021 14:41:35 +0200 Lukas Stevens Add empty line draft closure-solver
Thu, 23 Sep 2021 14:27:33 +0200 Lukas Stevens merged; closure-solver
Thu, 23 Sep 2021 14:11:55 +0200 Lukas Stevens Revert changes to order solver closure-solver
Thu, 23 Sep 2021 12:03:29 +0000 Lukas Stevens Another attempt to fix the tactic closure-solver
Thu, 23 Sep 2021 11:26:15 +0200 Lukas Stevens merged; closure-solver
Thu, 23 Sep 2021 11:30:49 +0200 desharna updated to Metis 2.4 (release 20200713)
Thu, 23 Sep 2021 11:02:25 +0200 Lukas Stevens merged;
Wed, 22 Sep 2021 22:28:56 +0200 wenzelm avoid problems with launch4j and jdk-17;
Wed, 22 Sep 2021 21:27:44 +0200 wenzelm update to jdk-17+35 (LTS);
Wed, 22 Sep 2021 21:20:36 +0200 wenzelm tuned message;
Wed, 22 Sep 2021 20:18:28 +0200 wenzelm unused since 398b7bb9ebdd;
Wed, 22 Sep 2021 14:32:20 +0200 desharna merged
Wed, 22 Sep 2021 12:03:59 +0200 wenzelm proper NEWS;
Wed, 22 Sep 2021 11:58:45 +0200 wenzelm tuned NEWS;
Wed, 22 Sep 2021 13:09:34 +0000 Lukas Stevens merged; draft
Wed, 22 Sep 2021 12:41:40 +0200 desharna removed checks for non-commercial usage of Vampire as it is now under BSD licence
Wed, 22 Sep 2021 12:25:09 +0200 desharna enabled FOOL for Vampire in Sledgehammer
Wed, 22 Sep 2021 10:46:42 +0200 desharna used Vampire 4.5.1 in Sledgehammer
Tue, 21 Sep 2021 20:56:28 +0200 wenzelm clarified antiquotations;
Tue, 21 Sep 2021 20:56:23 +0200 wenzelm clarified antiquotations;
Tue, 21 Sep 2021 20:56:06 +0200 wenzelm clarified antiquotations;
Tue, 21 Sep 2021 19:42:30 +0200 wenzelm clarified partial application: immediate check of object-logic, and avoidance of context within closure;
Tue, 21 Sep 2021 16:23:33 +0200 wenzelm merged
Tue, 21 Sep 2021 13:14:18 +0200 wenzelm clarified antiquotations;
Tue, 21 Sep 2021 13:12:14 +0200 wenzelm ML antiquotations for object-logic judgment;
Tue, 21 Sep 2021 12:35:38 +0200 wenzelm proper Sign.const_typargs via Theory.add_deps_const/Theory.const_dep;
Tue, 21 Sep 2021 12:25:40 +0200 wenzelm clarified modules;
Tue, 21 Sep 2021 12:08:41 +0200 wenzelm clarified modules;
Tue, 21 Sep 2021 11:34:58 +0200 wenzelm more uniform syntax;
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 tip