equal
deleted
inserted
replaced
143 recomputed with "apsnd (ATP_Util.map_prod |
143 recomputed with "apsnd (ATP_Util.map_prod |
144 Sledgehammer.short_string_of_sledgehammer_outcome single)". |
144 Sledgehammer.short_string_of_sledgehammer_outcome single)". |
145 INCOMPATIBILITY. |
145 INCOMPATIBILITY. |
146 - Added support for TX0 and TX1 TPTP formats and $ite/$let expressions |
146 - Added support for TX0 and TX1 TPTP formats and $ite/$let expressions |
147 in TH0 and TH1. |
147 in TH0 and TH1. |
|
148 - Added support for cvc5. |
148 - Replaced option "sledgehammer_atp_dest_dir" by |
149 - Replaced option "sledgehammer_atp_dest_dir" by |
149 "sledgehammer_atp_problem_dest_dir", for problem files, and |
150 "sledgehammer_atp_problem_dest_dir", for problem files, and |
150 "sledgehammer_atp_proof_dest_dir", for proof files. Minor INCOMPATIBILITY. |
151 "sledgehammer_atp_proof_dest_dir", for proof files. Minor INCOMPATIBILITY. |
151 - Removed support for experimental prover 'z3_tptp'. |
152 - Removed support for experimental prover 'z3_tptp'. |
152 - The fastest successfully preplayed proof is always suggested. |
153 - The fastest successfully preplayed proof is always suggested. |