src/ZF/Resid/Reduction.thy
changeset 1401 0c439768f45c
parent 1155 928a16e02f9f
child 1478 2b8c2a7547ab
     1.1 --- a/src/ZF/Resid/Reduction.thy	Fri Dec 08 19:48:15 1995 +0100
     1.2 +++ b/src/ZF/Resid/Reduction.thy	Sat Dec 09 13:36:11 1995 +0100
     1.3 @@ -8,8 +8,8 @@
     1.4  Reduction = Terms+
     1.5  
     1.6  consts
     1.7 -  Sred1, Sred,  Spar_red1,Spar_red    :: "i"
     1.8 -  "-1->","--->","=1=>",   "===>"      :: "[i,i]=>o" (infixl 50)
     1.9 +  Sred1, Sred,  Spar_red1,Spar_red    :: i
    1.10 +  "-1->","--->","=1=>",   "===>"      :: [i,i]=>o (infixl 50)
    1.11  
    1.12  translations
    1.13    "a -1-> b" == "<a,b>:Sred1"