src/ZF/ex/Comb.thy
changeset 1702 4aa538e82f76
parent 1478 2b8c2a7547ab
child 11316 b4e71bd751e4
     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