NEWS
changeset 20136 8e92a8f9720b
parent 20118 0c1ec587a5a8
child 20169 52173f7687fd
equal deleted inserted replaced
20135:5a6b33268bb6 20136:8e92a8f9720b
   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.