changeset 1401 | 0c439768f45c |
parent 1155 | 928a16e02f9f |
child 1478 | 2b8c2a7547ab |
--- a/src/ZF/Resid/Residuals.thy Fri Dec 08 19:48:15 1995 +0100 +++ b/src/ZF/Resid/Residuals.thy Sat Dec 09 13:36:11 1995 +0100 @@ -9,9 +9,9 @@ Residuals = Substitution+ consts - Sres :: "i" - residuals :: "[i,i,i]=>i" - "|>" :: "[i,i]=>i" (infixl 70) + Sres :: i + residuals :: [i,i,i]=>i + "|>" :: [i,i]=>i (infixl 70) translations "residuals(u,v,w)" == "<u,v,w>:Sres"