src/ZF/Resid/Conversion.thy
changeset 1401 0c439768f45c
parent 1048 5ba0314f8214
child 1478 2b8c2a7547ab
     1.1 --- a/src/ZF/Resid/Conversion.thy	Fri Dec 08 19:48:15 1995 +0100
     1.2 +++ b/src/ZF/Resid/Conversion.thy	Sat Dec 09 13:36:11 1995 +0100
     1.3 @@ -9,10 +9,10 @@
     1.4  Conversion = Confluence+
     1.5  
     1.6  consts
     1.7 -  Sconv1	:: "i"
     1.8 -  "<-1->"	:: "[i,i]=>o" (infixl 50)
     1.9 -  Sconv		:: "i"
    1.10 -  "<--->"	:: "[i,i]=>o" (infixl 50)
    1.11 +  Sconv1	:: i
    1.12 +  "<-1->"	:: [i,i]=>o (infixl 50)
    1.13 +  Sconv		:: i
    1.14 +  "<--->"	:: [i,i]=>o (infixl 50)
    1.15  
    1.16  translations
    1.17    "a<-1->b"    == "<a,b>:Sconv1"