equal
deleted
inserted
replaced
4 *) |
4 *) |
5 |
5 |
6 header {* A SAT-based Sudoku Solver *} |
6 header {* A SAT-based Sudoku Solver *} |
7 |
7 |
8 theory Sudoku |
8 theory Sudoku |
9 imports Main |
9 imports Main "../Library/Refute" |
10 begin |
10 begin |
11 |
11 |
12 text {* |
12 text {* |
13 Please make sure you are using an efficient SAT solver (e.g., zChaff) |
13 Please make sure you are using an efficient SAT solver (e.g., zChaff) |
14 when loading this theory. See Isabelle's settings file for details. |
14 when loading this theory. See Isabelle's settings file for details. |