Mon, 11 Mar 2024 21:11:23 +0100 sketch & explore: reduce unnecessary type constraints
Simon Wimmer <wimmers@in.tum.de> [Mon, 11 Mar 2024 21:11:23 +0100] rev 79902
sketch & explore: reduce unnecessary type constraints
Mon, 11 Mar 2024 21:20:36 +0100 sketch & explore: replace functionality of `sketch` by more useful `nxsketch` (and remove `nxsketch`)
Simon Wimmer <wimmers@in.tum.de> [Mon, 11 Mar 2024 21:20:36 +0100] rev 79901
sketch & explore: replace functionality of `sketch` by more useful `nxsketch` (and remove `nxsketch`)
Mon, 11 Mar 2024 21:31:18 +0100 sketch & explore: use Active.sendback_markup_command to preserve indentation of generated proof text
Simon Wimmer <wimmers@in.tum.de> [Mon, 11 Mar 2024 21:31:18 +0100] rev 79900
sketch & explore: use Active.sendback_markup_command to preserve indentation of generated proof text
Fri, 15 Mar 2024 17:57:03 +0100 change benchmark session to FOLP-ex (faster and less mean squared error than ZF-Constructible);
Fabian Huch <huch@in.tum.de> [Fri, 15 Mar 2024 17:57:03 +0100] rev 79899
change benchmark session to FOLP-ex (faster and less mean squared error than ZF-Constructible);
Thu, 14 Mar 2024 18:08:42 +0100 unused;
Fabian Huch <huch@in.tum.de> [Thu, 14 Mar 2024 18:08:42 +0100] rev 79898
unused;
Thu, 14 Mar 2024 17:27:40 +0100 tuned;
Fabian Huch <huch@in.tum.de> [Thu, 14 Mar 2024 17:27:40 +0100] rev 79897
tuned;
Thu, 14 Mar 2024 17:19:01 +0100 proper IPC for scheduled builds, following 7ae25372ab04;
Fabian Huch <huch@in.tum.de> [Thu, 14 Mar 2024 17:19:01 +0100] rev 79896
proper IPC for scheduled builds, following 7ae25372ab04;
Thu, 14 Mar 2024 15:46:39 +0100 proper check (amending 9aef1d1535ff);
Fabian Huch <huch@in.tum.de> [Thu, 14 Mar 2024 15:46:39 +0100] rev 79895
proper check (amending 9aef1d1535ff);
Thu, 14 Mar 2024 14:20:44 +0100 more synced options (following 6e5397fcc41b);
Fabian Huch <huch@in.tum.de> [Thu, 14 Mar 2024 14:20:44 +0100] rev 79894
more synced options (following 6e5397fcc41b);
Thu, 14 Mar 2024 08:24:48 +0000 avoid [no_atp] declations shadowing propositions from sledgehammer
haftmann [Thu, 14 Mar 2024 08:24:48 +0000] rev 79893
avoid [no_atp] declations shadowing propositions from sledgehammer
(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 tip