src/ZF/Resid/Substitution.thy
changeset 1401 0c439768f45c
parent 1155 928a16e02f9f
child 1478 2b8c2a7547ab
     1.1 --- a/src/ZF/Resid/Substitution.thy	Fri Dec 08 19:48:15 1995 +0100
     1.2 +++ b/src/ZF/Resid/Substitution.thy	Sat Dec 09 13:36:11 1995 +0100
     1.3 @@ -8,10 +8,10 @@
     1.4  Substitution = SubUnion +
     1.5  
     1.6  consts
     1.7 -  lift_rec	:: "[i,i]=> i"
     1.8 -  lift		:: "i=>i"
     1.9 -  subst_rec	:: "[i,i,i]=> i"
    1.10 -  "'/"          :: "[i,i]=>i"  (infixl 70)  (*subst*)
    1.11 +  lift_rec	:: [i,i]=> i
    1.12 +  lift		:: i=>i
    1.13 +  subst_rec	:: [i,i,i]=> i
    1.14 +  "'/"          :: [i,i]=>i  (infixl 70)  (*subst*)
    1.15  translations
    1.16    "lift(r)"  == "lift_rec(r,0)"
    1.17    "u/v" == "subst_rec(u,v,0)"