changeset 1401 | 0c439768f45c |
parent 1155 | 928a16e02f9f |
child 1478 | 2b8c2a7547ab |
--- a/src/ZF/Resid/Substitution.thy Fri Dec 08 19:48:15 1995 +0100 +++ b/src/ZF/Resid/Substitution.thy Sat Dec 09 13:36:11 1995 +0100 @@ -8,10 +8,10 @@ Substitution = SubUnion + consts - lift_rec :: "[i,i]=> i" - lift :: "i=>i" - subst_rec :: "[i,i,i]=> i" - "'/" :: "[i,i]=>i" (infixl 70) (*subst*) + lift_rec :: [i,i]=> i + lift :: i=>i + subst_rec :: [i,i,i]=> i + "'/" :: [i,i]=>i (infixl 70) (*subst*) translations "lift(r)" == "lift_rec(r,0)" "u/v" == "subst_rec(u,v,0)"