# HG changeset patch
# User paulson
# Date 952167761 -3600
# Node ID c169cd21fe42c35315e07e5d87f868af02bc66c4
# Parent  bcadeb9c709555305a712fa0a7f2ecce3a36d70f
tidied

diff -r bcadeb9c7095 -r c169cd21fe42 src/HOL/Induct/Mutil.thy
--- a/src/HOL/Induct/Mutil.thy	Sat Mar 04 11:52:42 2000 +0100
+++ b/src/HOL/Induct/Mutil.thy	Sat Mar 04 12:02:41 2000 +0100
@@ -8,25 +8,25 @@
   Popularized as the Mutilated Checkerboard Problem by J McCarthy
 *)
 
-Mutil = Finite +
-consts
-  domino  :: "(nat*nat)set set"
-  tiling  :: "'a set set => 'a set set"
-  below   :: "nat => nat set"
-  evnodd  :: "[(nat*nat)set, nat] => (nat*nat)set"
+Mutil = Main +
 
+consts    domino :: "(nat*nat)set set"
 inductive domino
   intrs
     horiz  "{(i, j), (i, Suc j)} : domino"
     vertl  "{(i, j), (Suc i, j)} : domino"
 
+consts     tiling :: "'a set set => 'a set set"
 inductive "tiling A"
   intrs
     empty  "{} : tiling A"
     Un     "[| a: A;  t: tiling A;  a <= -t |] ==> a Un t : tiling A"
 
-defs
-  below_def  "below n    == {i. i<n}"
-  evnodd_def "evnodd A b == A Int {(i,j). (i+j) mod 2 = b}"
+constdefs
+  below   :: "nat => nat set"
+   "below n    == {i. i<n}"
+  
+  evnodd  :: "[(nat*nat)set, nat] => (nat*nat)set"
+   "evnodd A b == A Int {(i,j). (i+j) mod 2 = b}"
 
 end