# HG changeset patch
# User paulson
# Date 830855289 -7200
# Node ID 4aa538e82f7681424c277aa401cb641a770eb66c
# Parent  a26fbeaaaabd86dc8b5d97eafe33c08fafddb8e2
Cosmetic re-ordering of declarations

diff -r a26fbeaaaabd -r 4aa538e82f76 src/ZF/ex/Comb.thy
--- a/src/ZF/ex/Comb.thy	Mon Apr 29 20:15:33 1996 +0200
+++ b/src/ZF/ex/Comb.thy	Tue Apr 30 11:08:09 1996 +0200
@@ -17,7 +17,7 @@
 
 (** Datatype definition of combinators S and K, with infixed application **)
 consts comb :: i
-datatype (* <= "univ(0)" *)
+datatype
   "comb" = K
          | S
          | "#" ("p: comb", "q: comb")   (infixl 90)
@@ -67,16 +67,13 @@
 
 
 (*Misc definitions*)
-consts
-  diamond   :: i => o
-  I         :: i
-
-defs
+constdefs
+  I :: i
+  "I == S#K#K"
 
-  diamond_def "diamond(r) == ALL x y. <x,y>:r --> 
-                            (ALL y'. <x,y'>:r --> 
-                                 (EX z. <y,z>:r & <y',z> : r))"
-
-  I_def       "I == S#K#K"
+  diamond :: i => o
+  "diamond(r) == ALL x y. <x,y>:r --> 
+                          (ALL y'. <x,y'>:r --> 
+                                   (EX z. <y,z>:r & <y',z> : r))"
 
 end
diff -r a26fbeaaaabd -r 4aa538e82f76 src/ZF/ex/Mutil.thy
--- a/src/ZF/ex/Mutil.thy	Mon Apr 29 20:15:33 1996 +0200
+++ b/src/ZF/ex/Mutil.thy	Tue Apr 30 11:08:09 1996 +0200
@@ -3,14 +3,16 @@
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1996  University of Cambridge
 
-The Mutilated Checkerboard Problem, formalized inductively
+The Mutilated Chess Board Problem, formalized inductively
+  Originator is Max Black, according to J A Robinson.
+  Popularized as the Mutilated Checkerboard Problem by J McCarthy
 *)
 
 Mutil = CardinalArith +
 consts
   domino  :: i
+  tiling  :: i=>i
   evnodd  :: [i,i]=>i
-  tiling  :: i=>i
 
 inductive
   domains "domino" <= "Pow(nat*nat)"
@@ -20,9 +22,6 @@
   type_intrs "[empty_subsetI, cons_subsetI, PowI, SigmaI, nat_succI]"
 
 
-defs
-  evnodd_def "evnodd(A,b) == {z:A. EX i j. z=<i,j> & (i#+j) mod 2 = b}"
-
 inductive
     domains "tiling(A)" <= "Pow(Union(A))"
   intrs
@@ -31,4 +30,7 @@
   type_intrs "[empty_subsetI, Union_upper, Un_least, PowI]"
   type_elims "[make_elim PowD]"
 
+defs
+  evnodd_def "evnodd(A,b) == {z:A. EX i j. z=<i,j> & (i#+j) mod 2 = b}"
+
 end