NEWS
changeset 58990 b66788d19c0f
parent 58963 26bf09b95dda
child 58999 ed09ae4ea2d8
equal deleted inserted replaced
58989:99831590def5 58990:b66788d19c0f
   165 
   165 
   166 * Library/Sum_of_Squares: simplified and improved "sos" method. Always
   166 * Library/Sum_of_Squares: simplified and improved "sos" method. Always
   167 use local CSDP executable, which is much faster than the NEOS server.
   167 use local CSDP executable, which is much faster than the NEOS server.
   168 The "sos_cert" functionality is invoked as "sos" with additional
   168 The "sos_cert" functionality is invoked as "sos" with additional
   169 argument. Minor INCOMPATIBILITY.
   169 argument. Minor INCOMPATIBILITY.
       
   170 
       
   171 * HOL-Decision_Procs:
       
   172   - New counterexample generator quickcheck[approximation] for
       
   173     inequalities of transcendental functions.
       
   174     Uses hardware floating point arithmetic to randomly discover
       
   175     potential counterexamples. Counterexamples are certified with the
       
   176     'approximation' method.
       
   177     See HOL/Decision_Procs/ex/Approximation_Quickcheck_Ex.thy for
       
   178     examples.
   170 
   179 
   171 
   180 
   172 *** Document preparation ***
   181 *** Document preparation ***
   173 
   182 
   174 * Document headings work uniformly via the commands 'chapter',
   183 * Document headings work uniformly via the commands 'chapter',