src/HOL/Lambda/Lambda.ML

--- a/src/HOL/Lambda/Lambda.ML	Mon Nov 04 10:56:15 1996 +0100
+++ b/src/HOL/Lambda/Lambda.ML	Mon Nov 04 17:23:37 1996 +0100
@@ -16,16 +16,16 @@
 (* don't add r_into_rtrancl! *)
 AddSIs beta.intrs;
 
-val db_case_distinction =
-  rule_by_tactic(EVERY[etac thin_rl 2,etac thin_rl 2,etac thin_rl 3])db.induct;
+val dB_case_distinction =
+  rule_by_tactic(EVERY[etac thin_rl 2,etac thin_rl 2,etac thin_rl 3])dB.induct;
 
 (*** Congruence rules for ->> ***)
 
-goal Lambda.thy "!!s. s ->> s' ==> Fun s ->> Fun s'";
+goal Lambda.thy "!!s. s ->> s' ==> Abs s ->> Abs s'";
 by (etac rtrancl_induct 1);
 by (ALLGOALS(fast_tac (!claset addIs [rtrancl_into_rtrancl])));
-qed "rtrancl_beta_Fun";
-AddSIs [rtrancl_beta_Fun];
+qed "rtrancl_beta_Abs";
+AddSIs [rtrancl_beta_Abs];
 
 goal Lambda.thy "!!s. s ->> s' ==> s @ t ->> s' @ t";
 by (etac rtrancl_induct 1);
@@ -64,7 +64,7 @@
 
 goal Lambda.thy
   "!i k. i < Suc k --> lift (lift t i) (Suc k) = lift (lift t k) i";
-by (db.induct_tac "t" 1);
+by (dB.induct_tac "t" 1);
 by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if])
                                     addsolver (cut_trans_tac))));
 by (safe_tac HOL_cs);
@@ -73,7 +73,7 @@
 
 goal Lambda.thy "!i j s. j < Suc i --> \
 \         lift (t[s/j]) i = (lift t (Suc i)) [lift s i / j]";
-by (db.induct_tac "t" 1);
+by (dB.induct_tac "t" 1);
 by (ALLGOALS(asm_simp_tac (!simpset addsimps [pred_def,subst_Var,lift_lift]
                                 setloop (split_tac [expand_if,expand_nat_case])
                                 addsolver (cut_trans_tac))));
@@ -85,7 +85,7 @@
 goal Lambda.thy
   "!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 (dB.induct_tac "t" 1);
 by (ALLGOALS(asm_simp_tac (!simpset addsimps [subst_Var,lift_lift]
                                 setloop (split_tac [expand_if])
                                 addsolver (cut_trans_tac))));
@@ -94,7 +94,7 @@
 qed "lift_subst_lt";
 
 goal Lambda.thy "!k s. (lift t k)[s/k] = t";
-by (db.induct_tac "t" 1);
+by (dB.induct_tac "t" 1);
 by (ALLGOALS (asm_full_simp_tac (!simpset setloop (split_tac[expand_if]))));
 qed "subst_lift";
 Addsimps [subst_lift];
@@ -102,7 +102,7 @@
 
 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 (dB.induct_tac "t" 1);
 by (ALLGOALS(asm_simp_tac
       (!simpset addsimps [pred_def,subst_Var,lift_lift RS sym,lift_subst_lt]
                 setloop (split_tac [expand_if,expand_nat_case])
@@ -115,20 +115,20 @@
 (*** Equivalence proof for optimized substitution ***)
 
 goal Lambda.thy "!k. liftn 0 t k = t";
-by (db.induct_tac "t" 1);
+by (dB.induct_tac "t" 1);
 by (ALLGOALS(asm_simp_tac(addsplit(!simpset))));
 qed "liftn_0";
 Addsimps [liftn_0];
 
 goal Lambda.thy "!k. liftn (Suc n) t k = lift (liftn n t k) k";
-by (db.induct_tac "t" 1);
+by (dB.induct_tac "t" 1);
 by (ALLGOALS(asm_simp_tac(addsplit(!simpset))));
 by (fast_tac (HOL_cs addDs [add_lessD1]) 1);
 qed "liftn_lift";
 Addsimps [liftn_lift];
 
 goal Lambda.thy "!n. substn t s n = t[liftn n s 0 / n]";
-by (db.induct_tac "t" 1);
+by (dB.induct_tac "t" 1);
 by (ALLGOALS(asm_simp_tac(addsplit(!simpset))));
 qed "substn_subst_n";
 Addsimps [substn_subst_n];