diff -r b89462f9d5f1 -r ec86863e87c8 src/ZF/ex/Comb.thy
--- a/src/ZF/ex/Comb.thy	Mon Nov 28 19:48:30 1994 +0100
+++ b/src/ZF/ex/Comb.thy	Tue Nov 29 00:31:31 1994 +0100
@@ -71,7 +71,7 @@
   diamond   :: "i => o"
   I         :: "i"
 
-rules
+defs
 
   diamond_def "diamond(r) == ALL x y. <x,y>:r --> \
 \                            (ALL y'. <x,y'>:r --> \