[isabelle-dev] Orphaned theory src/HOL/Library/Sum_of_Squares_Remote

[Makarius]

On Fri, 13 Sep 2013, Florian Haftmann wrote:

> This theory brands itself as »Examples with remote CSDP« and contains
> nothing beyond some sos invocations.  It should be moved to HOL/ex.

I've made this in c6e679443adc as a reduced version of the examples from 
Sum_of_Squares.thy.  Files Sum_of_Squares.thy and 
Sum_of_Squares_Remote.thy being adjacent in that directory reminds of the 
semi-formal connection of the sources.

The remote version has to be a separate theory in order to allow the use 
of "condition = ISABELLE_FULL_TEST" in the session ROOT.

This arrangement is semi-finished, e.g. we've recently had instabilities 
of the CSDP server access again.  (It had also revealed mistakes in the 
use of parser combinators in the ML part, but I did not investigate 
further.)

I don't mind if Sum_of_Squares is further brushed up, but there should be 
a particular plan behind it, for example to support CSDP tools routinely 
as Isabelle component.


 	Makarius