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"