--- 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
--- 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