--- a/src/HOL/ex/Sudoku.thy Thu May 01 22:41:03 2014 +0200 +++ b/src/HOL/ex/Sudoku.thy Thu May 01 22:56:59 2014 +0200 @@ -6,7 +6,7 @@ header {* A SAT-based Sudoku Solver *} theory Sudoku -imports Main +imports Main "../Library/Refute" begin text {*