src/ZF/Rel.thy
changeset 753 ec86863e87c8
parent 435 ca5356bd315a
child 1155 928a16e02f9f
--- a/src/ZF/Rel.thy	Mon Nov 28 19:48:30 1994 +0100
+++ b/src/ZF/Rel.thy	Tue Nov 29 00:31:31 1994 +0100
@@ -12,7 +12,7 @@
     sym,asym,antisym,trans :: "i=>o"
     trans_on               :: "[i,i]=>o"	("trans[_]'(_')")
 
-rules
+defs
   refl_def     "refl(A,r) == (ALL x: A. <x,x> : r)"
 
   irrefl_def   "irrefl(A,r) == ALL x: A. <x,x> ~: r"