equal
deleted
inserted
replaced
474 |
474 |
475 * Tactics 'sat' and 'satx' reimplemented, several improvements: goals |
475 * Tactics 'sat' and 'satx' reimplemented, several improvements: goals |
476 no longer need to be stated as "<prems> ==> False", equivalences (i.e. |
476 no longer need to be stated as "<prems> ==> False", equivalences (i.e. |
477 "=" on type bool) are handled, variable names of the form "lit_<n>" |
477 "=" on type bool) are handled, variable names of the form "lit_<n>" |
478 are no longer reserved, significant speedup. |
478 are no longer reserved, significant speedup. |
|
479 |
|
480 * Tactics 'sat' and 'satx' can now replay MiniSat proof traces. zChaff is |
|
481 still supported as well. |
479 |
482 |
480 * inductive and datatype: provide projections of mutual rules, bundled |
483 * inductive and datatype: provide projections of mutual rules, bundled |
481 as foo_bar.inducts; |
484 as foo_bar.inducts; |
482 |
485 |
483 * Library: theory Accessible_Part has been move to main HOL. |
486 * Library: theory Accessible_Part has been move to main HOL. |