changeset 1401 | 0c439768f45c |
parent 1155 | 928a16e02f9f |
child 1478 | 2b8c2a7547ab |
--- a/src/ZF/Resid/SubUnion.thy Fri Dec 08 19:48:15 1995 +0100 +++ b/src/ZF/Resid/SubUnion.thy Sat Dec 09 13:36:11 1995 +0100 @@ -8,10 +8,10 @@ SubUnion = Redex + consts - Ssub,Scomp,Sreg :: "i" - "<==","~" :: "[i,i]=>o" (infixl 70) - un :: "[i,i]=>i" (infixl 70) - regular :: "i=>o" + Ssub,Scomp,Sreg :: i + "<==","~" :: [i,i]=>o (infixl 70) + un :: [i,i]=>i (infixl 70) + regular :: i=>o translations "a<==b" == "<a,b>:Ssub"