Wed, 08 Jan 2025 14:35:30 +0100 remove special cases for CVC4 that are actually unused (see also 6273d4c8325b and 1f1c5d85d232);
wenzelm [Wed, 08 Jan 2025 14:35:30 +0100] rev 81751
remove special cases for CVC4 that are actually unused (see also 6273d4c8325b and 1f1c5d85d232);
Wed, 08 Jan 2025 14:30:17 +0100 rebuild cvc5 component (still inactive);
wenzelm [Wed, 08 Jan 2025 14:30:17 +0100] rev 81750
rebuild cvc5 component (still inactive); more robust workaround on all platforms, avoid crash of "sledgehammer [cvc5]" seen on x86_64-linux after line 75 of "$AFP/thys/Boolos_Curious_Inference_Automated/Boolos_Curious_Inference_Automated.thy";
Wed, 08 Jan 2025 15:10:09 +0100 tuned spacing
desharna [Wed, 08 Jan 2025 15:10:09 +0100] rev 81749
tuned spacing
Wed, 08 Jan 2025 15:00:35 +0100 merged
desharna [Wed, 08 Jan 2025 15:00:35 +0100] rev 81748
merged
Wed, 08 Jan 2025 14:51:32 +0100 tuned Sledgehammer caching
desharna [Wed, 08 Jan 2025 14:51:32 +0100] rev 81747
tuned Sledgehammer caching
Mon, 23 Dec 2024 19:38:16 +0100 Rename "suggest_of" to "instantiate"
Lukas Bartl [Mon, 23 Dec 2024 19:38:16 +0100] rev 81746
Rename "suggest_of" to "instantiate"
Wed, 08 Jan 2025 05:38:13 +0100 merged
nipkow [Wed, 08 Jan 2025 05:38:13 +0100] rev 81745
merged
Wed, 08 Jan 2025 05:37:40 +0100 added lemmas
nipkow [Wed, 08 Jan 2025 05:37:40 +0100] rev 81744
added lemmas
Tue, 07 Jan 2025 22:07:46 +0100 discontinue old / inaccurate show_brackets (see also a4f09493d929 and ca9f5dbab880);
wenzelm [Tue, 07 Jan 2025 22:07:46 +0100] rev 81743
discontinue old / inaccurate show_brackets (see also a4f09493d929 and ca9f5dbab880);
Tue, 07 Jan 2025 21:39:38 +0100 more markup, notaly for LaTeX output: treat record fields as quasi-consts;
wenzelm [Tue, 07 Jan 2025 21:39:38 +0100] rev 81742
more markup, notaly for LaTeX output: treat record fields as quasi-consts;
(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 tip