# HG changeset patch
# User paulson
# Date 1024912587 -7200
# Node ID 0ffc4403f81178e92394cf54643bd273f5e3b820
# Parent  bb5f4faea1f39f510d7798e1147ed5e8699c2aae
tweaks

diff -r bb5f4faea1f3 -r 0ffc4403f811 src/ZF/Induct/FoldSet.ML
--- a/src/ZF/Induct/FoldSet.ML	Sun Jun 23 10:14:13 2002 +0200
+++ b/src/ZF/Induct/FoldSet.ML	Mon Jun 24 11:56:27 2002 +0200
@@ -89,8 +89,8 @@
 by (asm_simp_tac (simpset() addsimps 
     [Fin_into_Finite RS Finite_imp_cardinal_cons])  1);
 by (rtac impI 1);
-(** LEVEL 10 **)
-by (case_tac "x=xb" 1 THEN Auto_tac);
+(** LEVEL 14 **)
+by (case_tac "x=xb" 1 THEN Auto_tac); (*SLOW*)
 by (asm_full_simp_tac (simpset() addsimps [cons_lemma1]) 1);
 by (REPEAT(thin_tac "ALL x:A. ?u(x)" 1) THEN Blast_tac 1);
 (*case x ~= xb*)
@@ -104,9 +104,9 @@
 by (rtac succ_le_imp_le 2);
 by (hyp_subst_tac 2);
 by (subgoal_tac "Finite(cons(xb, Cb)) & x:cons(xb, Cb) " 2);
-by (asm_simp_tac (simpset() addsimps [Finite_imp_succ_cardinal_Diff, 
+by (asm_full_simp_tac (simpset() addsimps [Finite_imp_succ_cardinal_Diff, 
                        Fin_into_Finite RS Finite_imp_cardinal_cons]) 2);
-by (asm_simp_tac (simpset() addsimps [thm "Fin.consI" RS Fin_into_Finite]) 2);
+by (asm_simp_tac (simpset() addsimps [Fin_into_Finite]) 2);
 by (res_inst_tac [("C1", "Ca-{xb}"), ("e1","e"), ("A1", "A"), ("f1", "f")] 
     (Fin_imp_fold_set RS exE) 1);
 by (blast_tac (claset() addIs [Diff_subset RS Fin_subset]) 1);
@@ -337,12 +337,10 @@
 
 Goal "Finite(I) ==> (ALL i:I. Finite(C(i))) --> Finite(RepFun(I, C))";
 by (etac Finite_induct 1);
-by (auto_tac (claset(), simpset() addsimps [Finite_0]));
-by (stac (cons_eq RS sym) 1);
-by (auto_tac (claset() addIs [Finite_Un, Finite_cons, Finite_0], simpset()));
+by Auto_tac;
 qed_spec_mp "Finite_RepFun";
 
-Goal "!!I. Finite(I) \
+Goal "Finite(I) \
 \     ==> (ALL i:I. Finite(C(i))) --> \
 \         (ALL i:I. ALL j:I. i~=j --> C(i) Int C(j) = 0) --> \
 \         setsum(f, UN i:I. C(i)) = setsum (%i. setsum(f, C(i)), I)";