desharna [Tue, 25 Feb 2025 17:37:45 +0100] rev 82203
take chained facts into consideration in tactic hammer (from Jasmin)
desharna [Tue, 25 Feb 2025 17:37:41 +0100] rev 82202
initial work on Magnushammer-inspured tactic hammer (from Jasmin)
desharna [Tue, 25 Feb 2025 15:54:41 +0100] rev 82201
added lemmas monotone_on_sup_fun, monotone_on_inf_fun, antimonotone_on_sup_fun, antimonotone_on_inf_fun (thanks to Alexander Pach)
desharna [Tue, 25 Feb 2025 14:23:25 +0100] rev 82200
tuned options given to modern E
Testing 500 goals of the HOL-Library session with a timeout of 30 s resulted in the following results.
- No option: 9.4 % solved
- Option "--auto": 45 % solved
- Option "--auto-schedule": 46.8 % solved
nipkow [Fri, 21 Feb 2025 18:46:59 +0100] rev 82199
weakened type class (thanks to Alexander Pach)
wenzelm [Wed, 19 Feb 2025 11:11:14 +0100] rev 82198
back to post-release mode -- after fork point;
nipkow [Wed, 19 Feb 2025 10:12:35 +0100] rev 82197
added lemma
nipkow [Wed, 19 Feb 2025 09:26:48 +0100] rev 82196
tuned
wenzelm [Tue, 18 Feb 2025 19:59:42 +0100] rev 82195
obsolete;
wenzelm [Tue, 18 Feb 2025 19:07:06 +0100] rev 82194
prefer inlined sfx.txt;