--- a/src/ZF/Resid/Substitution.thy Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/Resid/Substitution.thy Thu Jun 22 17:13:05 1995 +0200
@@ -17,10 +17,10 @@
"u/v" == "subst_rec(u,v,0)"
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"
+ 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"
(* subst_rec(u,Var(i),k) = if k<i then Var(i-1)
@@ -30,15 +30,15 @@
subst_rec(u,App(b,f,a),k) = App(b,subst_rec(u,f,p),subst_rec(u,a,p))
*)
- subst_rec_def "subst_rec(u,t,kg) == \
-\ redex_rec(t, \
-\ %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. \
-\ Fun(m`(lift(r))`(succ(k)))), \
-\ %b x y m p.lam r:redexes.lam k:nat. \
-\ App(b,m`r`k,p`r`k))`u`kg"
+ subst_rec_def "subst_rec(u,t,kg) ==
+ redex_rec(t,
+ %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.
+ Fun(m`(lift(r))`(succ(k)))),
+ %b x y m p.lam r:redexes.lam k:nat.
+ App(b,m`r`k,p`r`k))`u`kg"
end