equal
deleted
inserted
replaced
4 Copyright 1996 University of Cambridge |
4 Copyright 1996 University of Cambridge |
5 *) |
5 *) |
6 |
6 |
7 header {* The Mutilated Chess Board Problem *} |
7 header {* The Mutilated Chess Board Problem *} |
8 |
8 |
9 theory Mutil = Main: |
9 theory Mutil imports Main begin |
10 |
10 |
11 text {* |
11 text {* |
12 The Mutilated Chess Board Problem, formalized inductively. |
12 The Mutilated Chess Board Problem, formalized inductively. |
13 |
13 |
14 Originator is Max Black, according to J A Robinson. Popularized as |
14 Originator is Max Black, according to J A Robinson. Popularized as |