src/ZF/ex/Comb.thy

 
 Comb = Datatype +
 
 (** 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)
 
 (** Inductive definition of contractions, -1->

     Ap    "[| p=1=>q;  r=1=>s |] ==> p#r =1=> q#s"
   type_intrs "comb.intrs"
 
 
 (*Misc definitions*)
-consts
-  diamond   :: i => o
-  I         :: i
+constdefs
+  I :: i
+  "I == S#K#K"
 
-defs
-
-  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