[isabelle-dev] NEWS: new internal proof-producing SAT solver

Makarius makarius at sketis.net
Mon May 12 14:15:00 CEST 2014

On Mon, 12 May 2014, Tjark Weber wrote:

> On Fri, 2014-05-09 at 12:00 +0200, Tjark Weber wrote:
>> Moreover, it is merely a historic accident that the theory is based on
>> Refute. [...]
> I am attaching a patch that replaces Refute with Nitpick in
> HOL/ex/Sudoku.thy.

Thanks.  I have pushed this as Isabelle/35ce6dab3f5e.


More information about the isabelle-dev mailing list