Tue, 01 Feb 2022 12:49:14 +0100 don't pass --auto-schedule to E indiscriminately -- use it instead of 'auto' in one slice
blanchet [Tue, 01 Feb 2022 12:49:14 +0100] rev 75053
don't pass --auto-schedule to E indiscriminately -- use it instead of 'auto' in one slice
Tue, 01 Feb 2022 12:48:33 +0100 careful with partial applications
blanchet [Tue, 01 Feb 2022 12:48:33 +0100] rev 75052
careful with partial applications
Tue, 01 Feb 2022 12:32:33 +0100 don't perform preplaying steps if preplaying is disabled
blanchet [Tue, 01 Feb 2022 12:32:33 +0100] rev 75051
don't perform preplaying steps if preplaying is disabled
Tue, 01 Feb 2022 12:14:43 +0100 adjust TPTP THF parser to give priority to @ over other operators, to parse Ehoh proofs
blanchet [Tue, 01 Feb 2022 12:14:43 +0100] rev 75050
adjust TPTP THF parser to give priority to @ over other operators, to parse Ehoh proofs
Tue, 01 Feb 2022 11:52:40 +0100 tuned punctuation
blanchet [Tue, 01 Feb 2022 11:52:40 +0100] rev 75049
tuned punctuation
Tue, 01 Feb 2022 11:51:41 +0100 handle TPTP '!=' more gracefully in Isar proof reconstruction
blanchet [Tue, 01 Feb 2022 11:51:41 +0100] rev 75048
handle TPTP '!=' more gracefully in Isar proof reconstruction
Tue, 01 Feb 2022 10:58:09 +0100 guard against duplicate lines in Zipperposition proofs
blanchet [Tue, 01 Feb 2022 10:58:09 +0100] rev 75047
guard against duplicate lines in Zipperposition proofs
Tue, 01 Feb 2022 09:21:50 +0100 tuning
blanchet [Tue, 01 Feb 2022 09:21:50 +0100] rev 75046
tuning
Tue, 01 Feb 2022 08:59:35 +0100 tuned NEWS
blanchet [Tue, 01 Feb 2022 08:59:35 +0100] rev 75045
tuned NEWS
Mon, 31 Jan 2022 16:09:23 +0100 compile HOL-TPTP
blanchet [Mon, 31 Jan 2022 16:09:23 +0100] rev 75044
compile HOL-TPTP
(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 tip