[isabelle-dev] proposal for new numeral representation

Tobias Nipkow nipkow at in.tum.de
Mon Dec 5 10:44:49 CET 2011

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.


More information about the isabelle-dev mailing list