195 Vampire 4.6 (with Open Source license) |
195 Vampire 4.6 (with Open Source license) |
196 veriT 2021.06-rmx |
196 veriT 2021.06-rmx |
197 Zipperposition 2.1 |
197 Zipperposition 2.1 |
198 - Adjusted default provers: |
198 - Adjusted default provers: |
199 cvc4 vampire verit e spass z3 zipperposition |
199 cvc4 vampire verit e spass z3 zipperposition |
|
200 - Adjusted Zipperposition's slicing. |
200 - Removed legacy "lam_lifting" (synonym for "lifting") from option |
201 - Removed legacy "lam_lifting" (synonym for "lifting") from option |
201 "lam_trans". Minor INCOMPATIBILITY. |
202 "lam_trans". Minor INCOMPATIBILITY. |
202 - Renamed "hide_lams" to "opaque_lifting" in option "lam_trans". Minor |
203 - Renamed "hide_lams" to "opaque_lifting" in option "lam_trans". Minor |
203 INCOMPATIBILITY. |
204 INCOMPATIBILITY. |
204 - Added "opaque_combs" to option "lam_trans": lambda expressions are |
205 - Added "opaque_combs" to option "lam_trans": lambda expressions are |
205 rewritten using combinators, but the combinators are kept opaque, |
206 rewritten using combinators, but the combinators are kept opaque, |
206 i.e. without definitions. |
207 i.e. without definitions. |
207 |
208 |
208 * Metis: Renamed option "hide_lams" to "opaque_lifting". Minor |
209 * Metis: |
209 INCOMPATIBILITY. |
210 - Renamed option "hide_lams" to "opaque_lifting". Minor INCOMPATIBILITY. |
|
211 - Updated the Metis prover underlying the "metis" proof method to |
|
212 version 2.4 (release 20200713). The new version fixes one |
|
213 implementation defect. Very slight INCOMPATIBILITY. |
210 |
214 |
211 * Theory HOL-Library.Lattice_Syntax has been superseded by bundle |
215 * Theory HOL-Library.Lattice_Syntax has been superseded by bundle |
212 "lattice_syntax": it can be used in a local context via 'include' or in |
216 "lattice_syntax": it can be used in a local context via 'include' or in |
213 a global theory via 'unbundle'. The opposite declarations are bundled as |
217 a global theory via 'unbundle'. The opposite declarations are bundled as |
214 "no_lattice_syntax". Minor INCOMPATIBILITY. |
218 "no_lattice_syntax". Minor INCOMPATIBILITY. |