| Tue, 25 Feb 2025 17:43:58 +0100 |
desharna |
tactic hammer documentation (from Jasmin)
|
file |
diff |
annotate
|
| Thu, 09 Jan 2025 13:18:37 +0100 |
Lukas Bartl |
tuned documentation and order of instantiated facts
|
file |
diff |
annotate
|
| Wed, 18 Dec 2024 11:02:56 +0100 |
desharna |
added documentation for new Sledehammer option "cache_dir"
|
file |
diff |
annotate
|
| Wed, 18 Dec 2024 10:43:44 +0100 |
desharna |
updated affiliation in Sledgehammer documentation
|
file |
diff |
annotate
|
| Thu, 31 Oct 2024 09:24:10 +0100 |
blanchet |
adjusted documentation
|
file |
diff |
annotate
|
| Fri, 25 Oct 2024 15:31:58 +0200 |
blanchet |
variable instantiation in Sledgehammer and Metis
|
file |
diff |
annotate
|
| Wed, 10 Apr 2024 11:44:25 +0200 |
wenzelm |
rename \undef to \undefined to avoid problems with MacTeX 2014 or Ubuntu 24.04 beta;
|
file |
diff |
annotate
|
| Wed, 14 Jun 2023 15:47:27 +0200 |
blanchet |
disable 'falsify' and 'abduce' in Sledgehammer by default, since they don't seem to be very useful in practice
|
file |
diff |
annotate
|
| Wed, 01 Mar 2023 08:00:51 +0100 |
blanchet |
adopt terminology suggested by Larry Paulson
|
file |
diff |
annotate
|
| Wed, 01 Mar 2023 08:00:51 +0100 |
blanchet |
tweaked abduction in Sledgehammer
|
file |
diff |
annotate
|
| Wed, 01 Mar 2023 08:00:51 +0100 |
blanchet |
slightly more documentation
|
file |
diff |
annotate
|
| Wed, 01 Mar 2023 08:00:51 +0100 |
blanchet |
updated documentation
|
file |
diff |
annotate
|
| Wed, 01 Mar 2023 08:00:51 +0100 |
blanchet |
implemented ad hoc abduction in Sledgehammer with E
|
file |
diff |
annotate
|
| Wed, 15 Feb 2023 10:56:23 +0100 |
blanchet |
added refute mode to Sledgehammer to find 'counterexamples'
|
file |
diff |
annotate
|
| Wed, 17 Aug 2022 18:20:10 +0200 |
blanchet |
tweaked generation of Isar proofs
|
file |
diff |
annotate
|