equal
deleted
inserted
replaced
212 - Renamed "hide_lams" to "opaque_lifting" in option "lam_trans". Minor |
212 - Renamed "hide_lams" to "opaque_lifting" in option "lam_trans". Minor |
213 INCOMPATIBILITY. |
213 INCOMPATIBILITY. |
214 - Added "opaque_combs" to option "lam_trans": lambda expressions are |
214 - Added "opaque_combs" to option "lam_trans": lambda expressions are |
215 rewritten using combinators, but the combinators are kept opaque, |
215 rewritten using combinators, but the combinators are kept opaque, |
216 i.e. without definitions. |
216 i.e. without definitions. |
|
217 |
|
218 * Nitpick: |
|
219 - External solver "MiniSat" is available for all supported Isabelle |
|
220 platforms (including Windows and ARM); while "MiniSat_JNI" only |
|
221 works for Intel Linux and macOS. |
217 |
222 |
218 * Metis: |
223 * Metis: |
219 - Renamed option "hide_lams" to "opaque_lifting". Minor INCOMPATIBILITY. |
224 - Renamed option "hide_lams" to "opaque_lifting". Minor INCOMPATIBILITY. |
220 - Updated the Metis prover underlying the "metis" proof method to |
225 - Updated the Metis prover underlying the "metis" proof method to |
221 version 2.4 (release 20200713). The new version fixes one |
226 version 2.4 (release 20200713). The new version fixes one |