Tue, 25 Feb 2025 17:43:53 +0100 |
desharna |
tuned time slicing (from Jasmin)
|
changeset |
files
|
Tue, 25 Feb 2025 17:43:48 +0100 |
desharna |
tuning time slices in Sledgehammer (from Jasmin)
|
changeset |
files
|
Tue, 25 Feb 2025 17:43:33 +0100 |
desharna |
don't rerun tactic in minimizer -- this just redoes the same proof search again (from Jasmin)
|
changeset |
files
|
Tue, 25 Feb 2025 17:41:52 +0100 |
desharna |
rescale Sledgehammer slice factor (to allow smaller time slices for tactics like auto) (from Jasmin)
|
changeset |
files
|
Tue, 25 Feb 2025 17:37:45 +0100 |
desharna |
take chained facts into consideration in tactic hammer (from Jasmin)
|
changeset |
files
|
Tue, 25 Feb 2025 17:37:41 +0100 |
desharna |
initial work on Magnushammer-inspured tactic hammer (from Jasmin)
|
changeset |
files
|
Tue, 25 Feb 2025 15:54:41 +0100 |
desharna |
added lemmas monotone_on_sup_fun, monotone_on_inf_fun, antimonotone_on_sup_fun, antimonotone_on_inf_fun (thanks to Alexander Pach)
|
changeset |
files
|
Tue, 25 Feb 2025 14:23:25 +0100 |
desharna |
tuned options given to modern E
|
changeset |
files
|
Fri, 21 Feb 2025 18:46:59 +0100 |
nipkow |
weakened type class (thanks to Alexander Pach)
|
changeset |
files
|
Wed, 19 Feb 2025 11:11:14 +0100 |
wenzelm |
back to post-release mode -- after fork point;
|
changeset |
files
|
Wed, 19 Feb 2025 10:12:35 +0100 |
nipkow |
added lemma
|
changeset |
files
|
Wed, 19 Feb 2025 09:26:48 +0100 |
nipkow |
tuned
|
changeset |
files
|