Cosmetic re-ordering of declarations
authorpaulson
Tue Apr 30 11:08:09 1996 +0200 (1996-04-30)
changeset 17024aa538e82f76
parent 1701 a26fbeaaaabd
child 1703 e22ad43bab5f
Cosmetic re-ordering of declarations
src/ZF/ex/Comb.thy
src/ZF/ex/Mutil.thy
     1.1 --- a/src/ZF/ex/Comb.thy	Mon Apr 29 20:15:33 1996 +0200
     1.2 +++ b/src/ZF/ex/Comb.thy	Tue Apr 30 11:08:09 1996 +0200
     1.3 @@ -17,7 +17,7 @@
     1.4  
     1.5  (** Datatype definition of combinators S and K, with infixed application **)
     1.6  consts comb :: i
     1.7 -datatype (* <= "univ(0)" *)
     1.8 +datatype
     1.9    "comb" = K
    1.10           | S
    1.11           | "#" ("p: comb", "q: comb")   (infixl 90)
    1.12 @@ -67,16 +67,13 @@
    1.13  
    1.14  
    1.15  (*Misc definitions*)
    1.16 -consts
    1.17 -  diamond   :: i => o
    1.18 -  I         :: i
    1.19 -
    1.20 -defs
    1.21 +constdefs
    1.22 +  I :: i
    1.23 +  "I == S#K#K"
    1.24  
    1.25 -  diamond_def "diamond(r) == ALL x y. <x,y>:r --> 
    1.26 -                            (ALL y'. <x,y'>:r --> 
    1.27 -                                 (EX z. <y,z>:r & <y',z> : r))"
    1.28 -
    1.29 -  I_def       "I == S#K#K"
    1.30 +  diamond :: i => o
    1.31 +  "diamond(r) == ALL x y. <x,y>:r --> 
    1.32 +                          (ALL y'. <x,y'>:r --> 
    1.33 +                                   (EX z. <y,z>:r & <y',z> : r))"
    1.34  
    1.35  end
     2.1 --- a/src/ZF/ex/Mutil.thy	Mon Apr 29 20:15:33 1996 +0200
     2.2 +++ b/src/ZF/ex/Mutil.thy	Tue Apr 30 11:08:09 1996 +0200
     2.3 @@ -3,14 +3,16 @@
     2.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.5      Copyright   1996  University of Cambridge
     2.6  
     2.7 -The Mutilated Checkerboard Problem, formalized inductively
     2.8 +The Mutilated Chess Board Problem, formalized inductively
     2.9 +  Originator is Max Black, according to J A Robinson.
    2.10 +  Popularized as the Mutilated Checkerboard Problem by J McCarthy
    2.11  *)
    2.12  
    2.13  Mutil = CardinalArith +
    2.14  consts
    2.15    domino  :: i
    2.16 +  tiling  :: i=>i
    2.17    evnodd  :: [i,i]=>i
    2.18 -  tiling  :: i=>i
    2.19  
    2.20  inductive
    2.21    domains "domino" <= "Pow(nat*nat)"
    2.22 @@ -20,9 +22,6 @@
    2.23    type_intrs "[empty_subsetI, cons_subsetI, PowI, SigmaI, nat_succI]"
    2.24  
    2.25  
    2.26 -defs
    2.27 -  evnodd_def "evnodd(A,b) == {z:A. EX i j. z=<i,j> & (i#+j) mod 2 = b}"
    2.28 -
    2.29  inductive
    2.30      domains "tiling(A)" <= "Pow(Union(A))"
    2.31    intrs
    2.32 @@ -31,4 +30,7 @@
    2.33    type_intrs "[empty_subsetI, Union_upper, Un_least, PowI]"
    2.34    type_elims "[make_elim PowD]"
    2.35  
    2.36 +defs
    2.37 +  evnodd_def "evnodd(A,b) == {z:A. EX i j. z=<i,j> & (i#+j) mod 2 = b}"
    2.38 +
    2.39  end