| Thu, 07 Aug 2025 21:40:03 +0200 |
wenzelm |
avoid legacy operations;
|
file |
diff |
annotate
|
| Mon, 12 May 2025 13:02:52 +0200 |
Lukas Bartl |
clarify Sledgehammer instantiations without preplay (dont_preplay option and tactic provers)
|
file |
diff |
annotate
|
| Thu, 24 Apr 2025 14:25:12 +0200 |
desharna |
proper command message for Sledgehammer's proof methods
|
file |
diff |
annotate
|
| Mon, 14 Apr 2025 13:57:48 +0200 |
desharna |
tuned
|
file |
diff |
annotate
|
| Mon, 31 Mar 2025 19:17:51 +0200 |
desharna |
tuned
|
file |
diff |
annotate
|
| Tue, 25 Feb 2025 17:37:41 +0100 |
desharna |
initial work on Magnushammer-inspured tactic hammer (from Jasmin)
|
file |
diff |
annotate
|
| Fri, 25 Oct 2024 15:31:58 +0200 |
blanchet |
variable instantiation in Sledgehammer and Metis
|
file |
diff |
annotate
|
| Fri, 20 Sep 2024 14:28:13 +0200 |
wenzelm |
clarified signature: more explicit operations;
|
file |
diff |
annotate
|
| Wed, 10 Jul 2024 08:37:54 +0200 |
nipkow |
take care of facts in cartouches
|
file |
diff |
annotate
|
| Wed, 29 May 2024 10:43:22 +0200 |
nipkow |
pretty-printing sledgehammer command: merge indexed theorems
|
file |
diff |
annotate
|
| Wed, 20 Mar 2024 12:26:52 +0100 |
desharna |
try proof method "order" in Sledgehammer's proof reconstruction
|
file |
diff |
annotate
|
| Mon, 02 Oct 2023 11:22:53 +0200 |
desharna |
used standard Time.compare in Sledgehammer's preplay
|
file |
diff |
annotate
|
| Mon, 25 Sep 2023 17:16:32 +0200 |
blanchet |
added argo
|
file |
diff |
annotate
|
| Mon, 22 Aug 2022 06:27:28 +0200 |
Mathias Fleury |
remove duplicate parsing for alethe; fix skolemization;
|
file |
diff |
annotate
|
| Mon, 31 Jan 2022 16:09:23 +0100 |
blanchet |
tweaked Auto Sledgehammer's behavior and output
|
file |
diff |
annotate
|
| Mon, 31 Jan 2022 16:09:23 +0100 |
blanchet |
further work on new Sledgehammer slicing
|
file |
diff |
annotate
|
| Tue, 13 Jul 2021 10:57:15 +0200 |
blanchet |
revisited ac28714b7478: more faithful preplaying with chained facts
|
file |
diff |
annotate
|
| Tue, 01 Dec 2020 15:29:54 +0100 |
desharna |
tuned proof preplay to explicitly refer to Z3 backend
|
file |
diff |
annotate
|
| Thu, 29 Oct 2020 16:07:41 +0100 |
desharna |
Added smt (verit) to Sledgehammer's proof preplay.
|
file |
diff |
annotate
|
| Thu, 08 Oct 2020 17:46:03 +0200 |
blanchet |
removed obsolete unmaintained experimental prover Pirate
|
file |
diff |
annotate
|
| Tue, 20 Aug 2019 11:01:05 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sun, 14 Aug 2016 12:26:09 +0200 |
blanchet |
killed final stops in Sledgehammer and friends
|
file |
diff |
annotate
|
| Sat, 16 Jul 2016 19:35:27 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 01 Feb 2016 19:57:58 +0100 |
blanchet |
preplaying of 'smt' and 'metis' more in sync with actual method
|
file |
diff |
annotate
|
| Sun, 13 Dec 2015 21:56:15 +0100 |
wenzelm |
more general types Proof.method / context_tactic;
|
file |
diff |
annotate
|
| Mon, 05 Oct 2015 23:03:50 +0200 |
blanchet |
further improved fine point w.r.t. replaying in the presence of chained facts and a non-empty meta-quantifier prefix + avoid printing internal names in backquotes
|
file |
diff |
annotate
|
| Mon, 01 Jun 2015 18:59:21 +0200 |
haftmann |
dropped dead config option
|
file |
diff |
annotate
|
| Thu, 28 May 2015 09:50:17 +0200 |
blanchet |
took out Sledgehammer minimizer optimization that breaks things
|
file |
diff |
annotate
|
| Sun, 03 May 2015 22:15:29 +0200 |
blanchet |
improved one-line preplaying (don't rely on 'using x by simp' to mean 'by (simp add: x)' and beware of inaccessible '(local.)this')
|
file |
diff |
annotate
|
| Wed, 26 Nov 2014 20:05:34 +0100 |
wenzelm |
renamed "pairself" to "apply2", in accordance to @{apply 2};
|
file |
diff |
annotate
|