178 - Reintroduced "show_skolems" option by popular demand. |
178 - Reintroduced "show_skolems" option by popular demand. |
179 - Renamed attribute: nitpick_def ~> nitpick_unfold. |
179 - Renamed attribute: nitpick_def ~> nitpick_unfold. |
180 INCOMPATIBILITY. |
180 INCOMPATIBILITY. |
181 |
181 |
182 * Sledgehammer: |
182 * Sledgehammer: |
|
183 - Use quasi-sound (and efficient) translations by default. |
|
184 - Added support for the following provers: E-ToFoF, LEO-II, Satallax, SNARK, |
|
185 Waldmeister, and Z3 with TPTP syntax. |
|
186 - Automatically preplay and minimize proofs before showing them if this can be |
|
187 done within reasonable time. |
183 - sledgehammer available_provers ~> sledgehammer supported_provers. |
188 - sledgehammer available_provers ~> sledgehammer supported_provers. |
184 INCOMPATIBILITY. |
189 INCOMPATIBILITY. |
185 - Added support for SNARK and ToFoF-E on SystemOnTPTP and for simply typed |
|
186 TPTP problems (TFF). |
|
187 - Added "preplay_timeout", "slicing", "type_enc", "sound", "max_mono_iters", |
190 - Added "preplay_timeout", "slicing", "type_enc", "sound", "max_mono_iters", |
188 and "max_new_mono_instances" options. |
191 and "max_new_mono_instances" options. |
189 - Removed "explicit_apply" and "full_types" options as well as "Full Types" |
192 - Removed "explicit_apply" and "full_types" options as well as "Full Types" |
190 Proof General menu item. INCOMPATIBILITY. |
193 Proof General menu item. INCOMPATIBILITY. |
191 |
194 |