equal
deleted
inserted
replaced
4 Lawrence C Paulson, Cambridge University Computer Laboratory (original scripts) |
4 Lawrence C Paulson, Cambridge University Computer Laboratory (original scripts) |
5 *) |
5 *) |
6 |
6 |
7 header {* The Mutilated Checker Board Problem *} |
7 header {* The Mutilated Checker Board Problem *} |
8 |
8 |
9 theory MutilatedCheckerboard = Main: |
9 theory MutilatedCheckerboard imports Main begin |
10 |
10 |
11 text {* |
11 text {* |
12 The Mutilated Checker Board Problem, formalized inductively. See |
12 The Mutilated Checker Board Problem, formalized inductively. See |
13 \cite{paulson-mutilated-board} and |
13 \cite{paulson-mutilated-board} and |
14 \url{http://isabelle.in.tum.de/library/HOL/Induct/Mutil.html} for the |
14 \url{http://isabelle.in.tum.de/library/HOL/Induct/Mutil.html} for the |