equal
deleted
inserted
replaced
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', |