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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev