# HG changeset patch
# User nipkow
# Date 804437581 -7200
# Node ID ab725b698cb2ff045801995f950d7de4f12414be
# Parent  e4d6b42be73a64a8d10e769e8b296c00bc3a30f8
Renamed some vars.

diff -r e4d6b42be73a -r ab725b698cb2 src/HOL/Lambda/Lambda.ML
--- a/src/HOL/Lambda/Lambda.ML	Thu Jun 29 16:50:14 1995 +0200
+++ b/src/HOL/Lambda/Lambda.ML	Thu Jun 29 16:53:01 1995 +0200
@@ -102,8 +102,8 @@
 val lambda_ss = lambda_ss addsimps [subst_eq,subst_gt,subst_lt];
 
 goal Lambda.thy
-  "!i k. i < Suc k --> lift (lift s i) (Suc k) = lift (lift s k) i";
-by(db.induct_tac "s" 1);
+  "!i k. i < Suc k --> lift (lift t i) (Suc k) = lift (lift t k) i";
+by(db.induct_tac "t" 1);
 by(ALLGOALS(asm_simp_tac lambda_ss));
 by(strip_tac 1);
 by (excluded_middle_tac "nat < i" 1);
@@ -130,9 +130,9 @@
 val lambda_ss = lambda_ss addsimps [lift_subst];
 
 goal Lambda.thy
-  "!i j u. i < Suc j -->\
-\         lift (v[u/j]) i = (lift v i) [lift u i / Suc j]";
-by(db.induct_tac "v" 1);
+  "!i j s. i < Suc j -->\
+\         lift (t[s/j]) i = (lift t i) [lift s i / Suc j]";
+by(db.induct_tac "t" 1);
 by(ALLGOALS(asm_simp_tac (lambda_ss addsimps [lift_lift])));
 by(strip_tac 1);
 by (excluded_middle_tac "nat < j" 1);
@@ -147,8 +147,8 @@
 by (asm_full_simp_tac (lambda_ss addsimps [less_SucI]) 1);
 qed "lift_subst_lt";
 
-goal Lambda.thy "!k v. (lift u k)[v/k] = u";
-by(db.induct_tac "u" 1);
+goal Lambda.thy "!k s. (lift t k)[s/k] = t";
+by(db.induct_tac "t" 1);
 by(ALLGOALS(asm_simp_tac lambda_ss));
 by(split_tac [expand_if] 1);
 by(ALLGOALS(asm_full_simp_tac lambda_ss));
@@ -156,9 +156,9 @@
 val lambda_ss = lambda_ss addsimps [subst_lift];
 
 
-goal Lambda.thy "!i j u w. i < Suc j --> \
-\ (v[lift w i / Suc j]) [u[w/j]/i] = (v[u/i])[w/j]";
-by(db.induct_tac "v" 1);
+goal Lambda.thy "!i j u v. i < Suc j --> \
+\ t[lift v i / Suc j][u[v/j]/i] = t[u/i][v/j]";
+by(db.induct_tac "t" 1);
 by (ALLGOALS(asm_simp_tac (lambda_ss addsimps
                    [lift_lift RS spec RS spec RS mp RS sym,lift_subst_lt])));
 by(strip_tac 1);
diff -r e4d6b42be73a -r ab725b698cb2 src/HOL/Lambda/ParRed.ML
--- a/src/HOL/Lambda/ParRed.ML	Thu Jun 29 16:50:14 1995 +0200
+++ b/src/HOL/Lambda/ParRed.ML	Thu Jun 29 16:53:01 1995 +0200
@@ -51,8 +51,8 @@
 
 (*** => ***)
 
-goal ParRed.thy "!s' n. s => s' --> lift s n => lift s' n";
-by(db.induct_tac "s" 1);
+goal ParRed.thy "!t' n. t => t' --> lift t n => lift t' n";
+by(db.induct_tac "t" 1);
 by(ALLGOALS(fast_tac (parred_cs addss parred_ss)));
 bind_thm("par_beta_lift", result() RS spec RS spec RS mp);
 val parred_ss = parred_ss addsimps [par_beta_lift];