Fri, 18 Feb 2022 16:56:56 +0100 wenzelm clarified directory;
Fri, 18 Feb 2022 15:07:43 +0100 wenzelm tuned whitespace;
Fri, 18 Feb 2022 14:03:45 +0100 wenzelm prefer strict equality, without implicit type conversion;
Fri, 18 Feb 2022 13:48:50 +0100 wenzelm tuned;
Fri, 18 Feb 2022 13:26:36 +0100 wenzelm auto-update by VSCode;
Fri, 18 Feb 2022 13:26:11 +0100 wenzelm more activationEvents, as proposed by Denis Paluca;
Fri, 18 Feb 2022 12:22:37 +0100 wenzelm tuned message;
Fri, 18 Feb 2022 12:20:30 +0100 wenzelm NEWS;
Fri, 18 Feb 2022 12:18:41 +0100 wenzelm run Isabelle/VSCode using local VSCodium installation;
Fri, 18 Feb 2022 11:54:43 +0100 wenzelm provide macos_exe, based on bin/codium from linux;
Fri, 18 Feb 2022 11:34:30 +0100 wenzelm clarified options;
Thu, 17 Feb 2022 19:42:16 +0000 haftmann Avoid overaggresive splitting.
Thu, 17 Feb 2022 19:42:15 +0000 haftmann more lemmas for distribution
Thu, 17 Feb 2022 19:42:15 +0000 haftmann Avoid overaggresive simplification.
Thu, 17 Feb 2022 19:40:30 +0100 wenzelm merged
Thu, 17 Feb 2022 19:00:14 +0100 wenzelm setup VSCode from VSCodium distribution;
Thu, 17 Feb 2022 12:22:47 +0100 wenzelm more robust package_dir, to increase chances that it works with IntelliJ IDEA;
Wed, 16 Feb 2022 14:35:33 +0100 desharna NEWS
Wed, 16 Feb 2022 14:24:05 +0100 desharna Mirabelle now considers goals preceding "unfolding" and "using" commands
Tue, 15 Feb 2022 16:42:15 +0000 paulson merged
Tue, 15 Feb 2022 13:00:05 +0000 paulson an assortment of new or stronger lemmas
Tue, 15 Feb 2022 16:16:53 +0100 wenzelm obsolete (reverting b3d6bb2ebf77): Isabelle/Naproche cache is now value-oriented;
Mon, 14 Feb 2022 16:41:48 +0100 blanchet print outcome of Sledgehammer search in panel
Mon, 14 Feb 2022 16:34:56 +0100 blanchet print Sledgehammer error message
Sat, 12 Feb 2022 07:52:34 +0100 haftmann updated documentation to current matter of affairs
Thu, 10 Feb 2022 19:38:12 +0100 wenzelm unused;
Thu, 10 Feb 2022 19:31:07 +0100 wenzelm clarified signature;
Thu, 10 Feb 2022 09:29:19 +0100 desharna merged
Wed, 09 Feb 2022 16:39:55 +0100 desharna added Isabelle identification to Mirabelle output
Wed, 09 Feb 2022 14:52:05 +0100 desharna uniformized fact selection for ATP and SMT in Sledgehammer
Wed, 09 Feb 2022 23:05:50 +0100 wenzelm provide cache for slow computations;
Wed, 09 Feb 2022 13:02:59 +0100 desharna used max_facts and fact_filter from slice for both ATP and SMT in sledgehammer
Wed, 09 Feb 2022 12:06:01 +0100 wenzelm more operations;
Wed, 09 Feb 2022 10:47:34 +0100 blanchet more liberal parsing of Sledgehammer options to allow empty lists (as suggested by Larry Paulson)
Mon, 07 Feb 2022 16:59:37 +0100 blanchet more robust TSTP proof parsing
Mon, 07 Feb 2022 15:26:22 +0100 blanchet added possibility of extra options to SMT slices
Fri, 04 Feb 2022 10:48:49 +0100 nipkow tuned output syntax: Hoare triples are now blocks
Thu, 03 Feb 2022 10:33:55 +0100 nipkow tuned output syntax: INV and VAR are now blocks
Wed, 02 Feb 2022 13:43:48 +0100 blanchet more precise slicing computation and output when not enough lemmas are available (e.g. with the 'only' syntax 'sledgehammer (lem1 lem2 lem3)')
Wed, 02 Feb 2022 13:34:52 +0100 blanchet enable induction in one of Zipperposition's slices
Tue, 01 Feb 2022 18:12:04 +0100 blanchet made sorting of Vampire facts more robust in the face of names that deviate from the standard scheme
Tue, 01 Feb 2022 17:33:12 +0100 blanchet robustly handle empty proof blocks in Isar proof output
Tue, 01 Feb 2022 17:11:26 +0100 blanchet propagate right result when enough proofs have been found
Tue, 01 Feb 2022 16:16:50 +0100 blanchet correctly parse E proofs that assume '=' and '!=' bind more tightly than connectives
Tue, 01 Feb 2022 14:54:31 +0100 blanchet don't lose error messages
Tue, 01 Feb 2022 12:49:14 +0100 blanchet don't pass --auto-schedule to E indiscriminately -- use it instead of 'auto' in one slice
Tue, 01 Feb 2022 12:48:33 +0100 blanchet careful with partial applications
Tue, 01 Feb 2022 12:32:33 +0100 blanchet don't perform preplaying steps if preplaying is disabled
Tue, 01 Feb 2022 12:14:43 +0100 blanchet adjust TPTP THF parser to give priority to @ over other operators, to parse Ehoh proofs
Tue, 01 Feb 2022 11:52:40 +0100 blanchet tuned punctuation
Tue, 01 Feb 2022 11:51:41 +0100 blanchet handle TPTP '!=' more gracefully in Isar proof reconstruction
Tue, 01 Feb 2022 10:58:09 +0100 blanchet guard against duplicate lines in Zipperposition proofs
Tue, 01 Feb 2022 09:21:50 +0100 blanchet tuning
Tue, 01 Feb 2022 08:59:35 +0100 blanchet tuned NEWS
Mon, 31 Jan 2022 16:09:23 +0100 blanchet compile HOL-TPTP
Mon, 31 Jan 2022 16:09:23 +0100 blanchet compile Metis_Examples
Mon, 31 Jan 2022 16:09:23 +0100 blanchet more NEWS
Mon, 31 Jan 2022 16:09:23 +0100 blanchet compile mirabelle
Mon, 31 Jan 2022 16:09:23 +0100 blanchet tweaked Auto Sledgehammer's behavior and output
Mon, 31 Jan 2022 16:09:23 +0100 blanchet updated NEWS
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 tip