[isabelle-dev] proposal for new numeral representation

[Tobias Nipkow]

Am 25/11/2011 16:56, schrieb Makarius:
> 
> 
>> Broken proof methods
>>
>> sos_cert
>>   some uses in Library/Sum_of_Squares.thy
> 
> BTW the regular "sos" method with the server communication is broken for
> some months already.  It would be nice if someone could volunteer to
> recover this nice student project of Philipp Meyer.

It wasn't broken, at least not on our side, and today I got the
confirmation that they have fixed the problem on the remote server.
Thanks for alerting me.

BTW it would be nice to report such errors right away instead of after
some months.

Tobias