[isabelle-dev] NEWS: simplified sos method

2014-10-08 Thread Makarius
* Library/Sum_of_Squares: simplified and improved sos method. Always use local CSDP executable, which is much faster than the NEOS server. The sos_cert functionality is invoked as sos with additional argument. Minor INCOMPATIBILITY. This refers to Isabelle/71cdb885b3bb. It is a general brush-up

[isabelle-dev] NEWS: parameterized antiquotations @{map N}, @{fold N} etc.

2014-10-08 Thread Makarius
*** ML *** * Basic combinators map, fold, fold_map, split_list are available as parameterized antiquotations, e.g. @{map 4} for lists of quadruples. This refers to Isabelle/9f10d82e8188. After seeing another split_list42 combinator, I could not resist to make a fully general solution once

[isabelle-dev] Remaining uses of Python?

2014-10-08 Thread Makarius
As a consequence of discontinuing the painfully slow and fragile SOS/NEOS server support in 71cdb885b3bb, there is presently no remaining use of Python in Isabelle tools. Are there potential uses in the future? Otherwhise I could just remove it from the list of Dependable system tools in

Re: [isabelle-dev] NEWS: update_cartouches

2014-10-08 Thread Tobias Nipkow
I have no opinion wrt PG but just don't let your update tool lose on the whole distribution because there are some files of mine where that would create discrepancies in the text. Tobias On 08/10/2014 00:25, Makarius wrote: *** System *** * The Isabelle tool update_cartouches changes theory