blanchet [Tue, 01 Feb 2022 12:32:33 +0100] rev 75051
don't perform preplaying steps if preplaying is disabled
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
blanchet [Tue, 01 Feb 2022 11:52:40 +0100] rev 75049
tuned punctuation
blanchet [Tue, 01 Feb 2022 11:51:41 +0100] rev 75048
handle TPTP '!=' more gracefully in Isar proof reconstruction
blanchet [Tue, 01 Feb 2022 10:58:09 +0100] rev 75047
guard against duplicate lines in Zipperposition proofs
blanchet [Tue, 01 Feb 2022 09:21:50 +0100] rev 75046
tuning
blanchet [Tue, 01 Feb 2022 08:59:35 +0100] rev 75045
tuned NEWS
blanchet [Mon, 31 Jan 2022 16:09:23 +0100] rev 75044
compile HOL-TPTP
blanchet [Mon, 31 Jan 2022 16:09:23 +0100] rev 75043
compile Metis_Examples
blanchet [Mon, 31 Jan 2022 16:09:23 +0100] rev 75042
more NEWS
blanchet [Mon, 31 Jan 2022 16:09:23 +0100] rev 75041
compile mirabelle
blanchet [Mon, 31 Jan 2022 16:09:23 +0100] rev 75040
tweaked Auto Sledgehammer's behavior and output
blanchet [Mon, 31 Jan 2022 16:09:23 +0100] rev 75039
updated NEWS
blanchet [Mon, 31 Jan 2022 16:09:23 +0100] rev 75038
removed experimental prover z3_tptp
blanchet [Mon, 31 Jan 2022 16:09:23 +0100] rev 75037
print more verbose information
blanchet [Mon, 31 Jan 2022 16:09:23 +0100] rev 75036
run all installed provers by default
blanchet [Mon, 31 Jan 2022 16:09:23 +0100] rev 75035
update slice options centrally
blanchet [Mon, 31 Jan 2022 16:09:23 +0100] rev 75034
further work on new Sledgehammer slicing
blanchet [Mon, 31 Jan 2022 16:09:23 +0100] rev 75033
tweaked verbose output
blanchet [Mon, 31 Jan 2022 16:09:23 +0100] rev 75032
tweak padding of prover slice schedule to include all provers
blanchet [Mon, 31 Jan 2022 16:09:23 +0100] rev 75031
implemented 'max_proofs' mechanism
blanchet [Mon, 31 Jan 2022 16:09:23 +0100] rev 75030
document new option 'max_proofs'
blanchet [Mon, 31 Jan 2022 16:09:23 +0100] rev 75029
crude implementation of centralized slicing
blanchet [Mon, 31 Jan 2022 16:09:23 +0100] rev 75028
removed obscure E option
blanchet [Mon, 31 Jan 2022 16:09:23 +0100] rev 75027
take 'induction_rules' into consideration, as well as 'max_facts' even when 'only' is set
blanchet [Mon, 31 Jan 2022 16:09:23 +0100] rev 75026
rationalize slicing format
blanchet [Mon, 31 Jan 2022 16:09:23 +0100] rev 75025
thread slices through
blanchet [Mon, 31 Jan 2022 16:09:23 +0100] rev 75024
simplified 'best_slice' data structure and made minor changes to slices