equal
deleted
inserted
replaced
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 - Added support for cvc5. |
|
149 - Generate Isar proofs by default when and only when the one-liner proof |
|
150 fails to replay and the Isar proof succeeds. |
149 - Replaced option "sledgehammer_atp_dest_dir" by |
151 - Replaced option "sledgehammer_atp_dest_dir" by |
150 "sledgehammer_atp_problem_dest_dir", for problem files, and |
152 "sledgehammer_atp_problem_dest_dir", for problem files, and |
151 "sledgehammer_atp_proof_dest_dir", for proof files. Minor INCOMPATIBILITY. |
153 "sledgehammer_atp_proof_dest_dir", for proof files. Minor INCOMPATIBILITY. |
152 - Removed support for experimental prover 'z3_tptp'. |
154 - Removed support for experimental prover 'z3_tptp'. |
153 - The fastest successfully preplayed proof is always suggested. |
155 - The fastest successfully preplayed proof is always suggested. |