--- a/src/ZF/Resid/Substitution.thy Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/Resid/Substitution.thy Fri Oct 10 18:23:31 1997 +0200
@@ -18,9 +18,9 @@
defs
lift_rec_def "lift_rec(r,kg) ==
- redex_rec(r,%i.(lam k:nat.if(i<k,Var(i),Var(succ(i)))),
- %x m.(lam k:nat.Fun(m`(succ(k)))),
- %b x y m p.lam k:nat.App(b,m`k,p`k))`kg"
+ redex_rec(r,%i.(lam k:nat. if(i<k,Var(i),Var(succ(i)))),
+ %x m.(lam k:nat. Fun(m`(succ(k)))),
+ %b x y m p. lam k:nat. App(b,m`k,p`k))`kg"
(* subst_rec(u,Var(i),k) = if k<i then Var(i-1)
@@ -32,12 +32,12 @@
*)
subst_rec_def "subst_rec(u,t,kg) ==
redex_rec(t,
- %i.(lam r:redexes.lam k:nat.
+ %i.(lam r:redexes. lam k:nat.
if(k<i,Var(i#-1),
if(k=i,r,Var(i)))),
- %x m.(lam r:redexes.lam k:nat.
+ %x m.(lam r:redexes. lam k:nat.
Fun(m`(lift(r))`(succ(k)))),
- %b x y m p.lam r:redexes.lam k:nat.
+ %b x y m p. lam r:redexes. lam k:nat.
App(b,m`r`k,p`r`k))`u`kg"