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