NEWS
changeset 58630 71cdb885b3bb
parent 58626 6c473ed0ac70
child 58634 9f10d82e8188
equal deleted inserted replaced
58629:a6a6cd499d4e 58630:71cdb885b3bb
   123 * List: renamed drop_Suc_conv_tl and nth_drop' to Cons_nth_drop_Suc
   123 * List: renamed drop_Suc_conv_tl and nth_drop' to Cons_nth_drop_Suc
   124 
   124 
   125 * New infrastructure for compiling, running, evaluating and testing
   125 * New infrastructure for compiling, running, evaluating and testing
   126   generated code in target languages in HOL/Library/Code_Test. See
   126   generated code in target languages in HOL/Library/Code_Test. See
   127   HOL/Codegenerator_Test/Code_Test* for examples.
   127   HOL/Codegenerator_Test/Code_Test* for examples.
       
   128 
       
   129 * Library/Sum_of_Squares: simplified and improved "sos" method. Always
       
   130 use local CSDP executable, which is much faster than the NEOS server.
       
   131 The "sos_cert" functionality is invoked as "sos" with additional
       
   132 argument. Minor INCOMPATIBILITY.
       
   133 
   128 
   134 
   129 *** ML ***
   135 *** ML ***
   130 
   136 
   131 * Tactical PARALLEL_ALLGOALS is the most common way to refer to
   137 * Tactical PARALLEL_ALLGOALS is the most common way to refer to
   132 PARALLEL_GOALS.
   138 PARALLEL_GOALS.