[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 bru

[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 and

[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 Ad

Re: [isabelle-dev] default cases rule

2014-10-08 Thread Makarius
On Fri, 5 Sep 2014, Christian Sternagel wrote: I forgot to check the NEWS ;) Just another advertisement of the "IDE" for the NEWS file, with the change from 3 days ago: changeset: 58542:19e062fbfea0 user:wenzelm date:Sun Oct 05 13:16:24 2014 +0200 files: src/Tools/jE

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 theor