466 "SAT4JLight" to "MiniSat_JNI", "zChaff_JNI", "BerkMin_Alloy", and |
466 "SAT4JLight" to "MiniSat_JNI", "zChaff_JNI", "BerkMin_Alloy", and |
467 "SAT4J_Light". INCOMPATIBILITY. |
467 "SAT4J_Light". INCOMPATIBILITY. |
468 - Removed "skolemize", "uncurry", "sym_break", "flatten_prop", |
468 - Removed "skolemize", "uncurry", "sym_break", "flatten_prop", |
469 "sharing_depth", and "show_skolems" options. INCOMPATIBILITY. |
469 "sharing_depth", and "show_skolems" options. INCOMPATIBILITY. |
470 - Removed "nitpick_intro" attribute. INCOMPATIBILITY. |
470 - Removed "nitpick_intro" attribute. INCOMPATIBILITY. |
|
471 |
|
472 * Method "induct" now takes instantiations of the form t, where t is not |
|
473 a variable, as a shorthand for "x == t", where x is a fresh variable. |
|
474 If this is not intended, t has to be enclosed in parentheses. |
|
475 By default, the equalities generated by definitional instantiations |
|
476 are pre-simplified, which may cause parameters of inductive cases |
|
477 to disappear, or may even delete some of the inductive cases. |
|
478 Use "induct (no_simp)" instead of "induct" to restore the old |
|
479 behaviour. The (no_simp) option is also understood by the "cases" |
|
480 and "nominal_induct" methods, which now perform pre-simplification, too. |
|
481 INCOMPATIBILITY. |
471 |
482 |
472 |
483 |
473 *** HOLCF *** |
484 *** HOLCF *** |
474 |
485 |
475 * Variable names in lemmas generated by the domain package have |
486 * Variable names in lemmas generated by the domain package have |