# HG changeset patch
# User paulson
# Date 962182655 -7200
# Node ID 6ef054f33f8355bdfc66c90451b151d17ce07eea
# Parent  422968aeed49d019c88bda696a3d7089b53ed60b
FORCED TO RENAME "W" DUE TO COMPOSE VARIABLE-CLASH BUG

diff -r 422968aeed49 -r 6ef054f33f83 src/ZF/InfDatatype.ML
--- a/src/ZF/InfDatatype.ML	Wed Jun 28 10:56:34 2000 +0200
+++ b/src/ZF/InfDatatype.ML	Wed Jun 28 10:57:35 2000 +0200
@@ -11,31 +11,31 @@
      transfer InfDatatype.thy Limit_VfromE 
    |> standard;
 
-Goal "[| f: W -> Vfrom(A,csucc(K));  |W| le K;  InfCard(K)  \
-\         |] ==> EX j. f: W -> Vfrom(A,j) & j < csucc(K)";
-by (res_inst_tac [("x", "UN w:W. LEAST i. f`w : Vfrom(A,i)")] exI 1);
+Goal "[| f: D -> Vfrom(A,csucc(K));  |D| le K;  InfCard(K) |]  \
+\     ==> EX j. f: D -> Vfrom(A,j) & j < csucc(K)";
+by (res_inst_tac [("x", "UN d:D. LEAST i. f`d : Vfrom(A,i)")] exI 1);
 by (rtac conjI 1);
 by (rtac le_UN_Ord_lt_csucc 2);
 by (rtac ballI 4  THEN
     etac fun_Limit_VfromE 4 THEN REPEAT_SOME assume_tac);
 by (fast_tac (claset() addEs [Least_le RS lt_trans1, ltE]) 2);
 by (rtac Pi_type 1);
-by (rename_tac "w" 2);
+by (rename_tac "d" 2);
 by (etac fun_Limit_VfromE 2 THEN REPEAT_SOME assume_tac);
-by (subgoal_tac "f`w : Vfrom(A, LEAST i. f`w : Vfrom(A,i))" 1);
+by (subgoal_tac "f`d : Vfrom(A, LEAST i. f`d : Vfrom(A,i))" 1);
 by (fast_tac (claset() addEs [LeastI, ltE]) 2);
 by (eresolve_tac [[subset_refl, UN_upper] MRS Vfrom_mono RS subsetD] 1);
 by (assume_tac 1);
 qed "fun_Vcsucc_lemma";
 
-Goal "[| W <= Vfrom(A,csucc(K));  |W| le K;  InfCard(K)     \
-\         |] ==> EX j. W <= Vfrom(A,j) & j < csucc(K)";
-by (asm_full_simp_tac (simpset() addsimps [subset_iff_id, fun_Vcsucc_lemma]) 1);
+Goal "[| D <= Vfrom(A,csucc(K));  |D| le K;  InfCard(K) |]    \
+\     ==> EX j. D <= Vfrom(A,j) & j < csucc(K)";
+by (asm_full_simp_tac (simpset() addsimps [subset_iff_id,fun_Vcsucc_lemma]) 1);
 qed "subset_Vcsucc";
 
 (*Version for arbitrary index sets*)
-Goal "[| |W| le K;  InfCard(K);  W <= Vfrom(A,csucc(K)) |] ==> \
-\         W -> Vfrom(A,csucc(K)) <= Vfrom(A,csucc(K))";
+Goal "[| |D| le K;  InfCard(K);  D <= Vfrom(A,csucc(K)) |] ==> \
+\         D -> Vfrom(A,csucc(K)) <= Vfrom(A,csucc(K))";
 by (safe_tac (claset() addSDs [fun_Vcsucc_lemma, subset_Vcsucc]));
 by (resolve_tac [Vfrom RS ssubst] 1);
 by (dtac fun_is_rel 1);
@@ -47,9 +47,9 @@
                       Limit_has_succ, Un_least_lt] 1));
 qed "fun_Vcsucc";
 
-Goal "[| f: W -> Vfrom(A, csucc(K));  |W| le K;  InfCard(K);        \
-\            W <= Vfrom(A,csucc(K))                                     \
-\         |] ==> f: Vfrom(A,csucc(K))";
+Goal "[| f: D -> Vfrom(A, csucc(K));  |D| le K;  InfCard(K);        \
+\        D <= Vfrom(A,csucc(K)) |]                                  \
+\      ==> f: Vfrom(A,csucc(K))";
 by (REPEAT (ares_tac [fun_Vcsucc RS subsetD] 1));
 qed "fun_in_Vcsucc";