Quickcheck returns variable assignments as counterexamples, which
allows to reveal the underspecification of functions under test.
For example, refuting "hd xs = x", it presents the variable
assignment xs = [] and x = a1 as a counterexample, assuming that
any property is false
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 s
