equal
deleted
inserted
replaced
7 |
7 |
8 theory Mutilated_Checkerboard |
8 theory Mutilated_Checkerboard |
9 imports Main |
9 imports Main |
10 begin |
10 begin |
11 |
11 |
12 text \<open>The Mutilated Checker Board Problem, formalized inductively. See @{cite |
12 text \<open> |
13 "paulson-mutilated-board"} for the original tactic script version.\<close> |
13 The Mutilated Checker Board Problem, formalized inductively. See @{cite |
|
14 "paulson-mutilated-board"} for the original tactic script version. |
|
15 \<close> |
14 |
16 |
15 subsection \<open>Tilings\<close> |
17 subsection \<open>Tilings\<close> |
16 |
18 |
17 inductive_set tiling :: "'a set set \<Rightarrow> 'a set set" |
19 inductive_set tiling :: "'a set set \<Rightarrow> 'a set set" |
18 for A :: "'a set set" |
20 for A :: "'a set set" |