src/ZF/Resid/Conversion.thy
changeset 1401 0c439768f45c
parent 1048 5ba0314f8214
child 1478 2b8c2a7547ab
--- a/src/ZF/Resid/Conversion.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/Resid/Conversion.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -9,10 +9,10 @@
 Conversion = Confluence+
 
 consts
-  Sconv1	:: "i"
-  "<-1->"	:: "[i,i]=>o" (infixl 50)
-  Sconv		:: "i"
-  "<--->"	:: "[i,i]=>o" (infixl 50)
+  Sconv1	:: i
+  "<-1->"	:: [i,i]=>o (infixl 50)
+  Sconv		:: i
+  "<--->"	:: [i,i]=>o (infixl 50)
 
 translations
   "a<-1->b"    == "<a,b>:Sconv1"