src/ZF/ex/Ramsey.thy
changeset 1401 0c439768f45c
parent 1155 928a16e02f9f
child 1478 2b8c2a7547ab
--- a/src/ZF/ex/Ramsey.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/ex/Ramsey.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -20,9 +20,9 @@
 
 Ramsey = Arith +
 consts
-  Symmetric   		:: "i=>o"
-  Atleast     		:: "[i,i]=>o"
-  Clique,Indept,Ramsey	:: "[i,i,i]=>o"
+  Symmetric   		:: i=>o
+  Atleast     		:: [i,i]=>o
+  Clique,Indept,Ramsey	:: [i,i,i]=>o
 
 defs