src/ZF/Rel.thy
changeset 1401 0c439768f45c
parent 1155 928a16e02f9f
child 1478 2b8c2a7547ab
--- a/src/ZF/Rel.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/Rel.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -8,9 +8,9 @@
 
 Rel = ZF +
 consts
-    refl,irrefl,equiv      :: "[i,i]=>o"
-    sym,asym,antisym,trans :: "i=>o"
-    trans_on               :: "[i,i]=>o"	("trans[_]'(_')")
+    refl,irrefl,equiv      :: [i,i]=>o
+    sym,asym,antisym,trans :: i=>o
+    trans_on               :: [i,i]=>o	("trans[_]'(_')")
 
 defs
   refl_def     "refl(A,r) == (ALL x: A. <x,x> : r)"