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

[Makarius]

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.


 	Makarius