NEWS
changeset 59965 7199ad93b744
parent 59958 4538d41e8e54
child 59967 2fcf41a626f7
equal deleted inserted replaced
59964:5c95c94952df 59965:7199ad93b744
   291     operations.
   291     operations.
   292 
   292 
   293 * Sledgehammer:
   293 * Sledgehammer:
   294   - CVC4 is now included with Isabelle instead of CVC3 and run by
   294   - CVC4 is now included with Isabelle instead of CVC3 and run by
   295     default.
   295     default.
       
   296   - Z3 is now always enabled by default, now that it is fully open
       
   297     source. The "z3_non_commercial" option is discontinued.
   296   - Minimization is now always enabled by default.
   298   - Minimization is now always enabled by default.
   297     Removed subcommand:
   299     Removed subcommand:
   298       min
   300       min
   299   - The proof reconstruction, both one-liners and Isar, has been
   301   - The proof reconstruction, both one-liners and Isar, has been
   300     dramatically improved.
   302     dramatically improved.