--- a/src/HOL/Induct/Mutil.thy Wed Jul 11 11:13:08 2007 +0200
+++ b/src/HOL/Induct/Mutil.thy Wed Jul 11 11:14:51 2007 +0200
@@ -15,18 +15,19 @@
the Mutilated Checkerboard Problem by J McCarthy.
*}
-consts tiling :: "'a set set => 'a set set"
-inductive "tiling A"
- intros
+inductive_set
+ tiling :: "'a set set => 'a set set"
+ for A :: "'a set set"
+ where
empty [simp, intro]: "{} \<in> tiling A"
- Un [simp, intro]: "[| a \<in> A; t \<in> tiling A; a \<inter> t = {} |]
+ | Un [simp, intro]: "[| a \<in> A; t \<in> tiling A; a \<inter> t = {} |]
==> a \<union> t \<in> tiling A"
-consts domino :: "(nat \<times> nat) set set"
-inductive domino
- intros
+inductive_set
+ domino :: "(nat \<times> nat) set set"
+ where
horiz [simp]: "{(i, j), (i, Suc j)} \<in> domino"
- vertl [simp]: "{(i, j), (Suc i, j)} \<in> domino"
+ | vertl [simp]: "{(i, j), (Suc i, j)} \<in> domino"
text {* \medskip Sets of squares of the given colour*}