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