src/HOL/Complex/CSeries.ML
changeset 14373 67a628beb981
parent 14334 6137d24eef79
     1.1 --- a/src/HOL/Complex/CSeries.ML	Tue Feb 03 10:19:21 2004 +0100
     1.2 +++ b/src/HOL/Complex/CSeries.ML	Tue Feb 03 11:06:36 2004 +0100
     1.3 @@ -37,7 +37,7 @@
     1.4  by (induct_tac "n" 1);
     1.5  by (Auto_tac);
     1.6  by (auto_tac (claset(),simpset() addsimps 
     1.7 -    [complex_add_mult_distrib2]));
     1.8 +    [right_distrib]));
     1.9  qed "sumc_mult";
    1.10  
    1.11  Goal "n < p --> sumc 0 n f + sumc n p f = sumc 0 p f";
    1.12 @@ -49,7 +49,7 @@
    1.13  Goal "n < p ==> sumc 0 p f + \
    1.14  \                - sumc 0 n f = sumc n p f";
    1.15  by (dres_inst_tac [("f1","f")] (sumc_split_add RS sym) 1);
    1.16 -by (asm_simp_tac (simpset() addsimps complex_add_ac) 1);
    1.17 +by (asm_simp_tac (simpset() addsimps add_ac) 1);
    1.18  qed "sumc_split_add_minus";
    1.19  
    1.20  Goal "cmod(sumc m n f) <= sumr m n (%i. cmod(f i))";
    1.21 @@ -67,7 +67,7 @@
    1.22  Goal "sumc 0 n (%i. r) = complex_of_real (real n) * r";
    1.23  by (induct_tac "n" 1);
    1.24  by (auto_tac (claset(),
    1.25 -              simpset() addsimps [complex_add_mult_distrib,
    1.26 +              simpset() addsimps [left_distrib,
    1.27                                    complex_of_real_add RS sym,
    1.28                                    real_of_nat_Suc]));
    1.29  qed "sumc_const";
    1.30 @@ -109,7 +109,7 @@
    1.31  by (induct_tac "na" 1);
    1.32  by (auto_tac (claset(),simpset() addsimps [left_distrib, Suc_diff_n,
    1.33                                        real_of_nat_Suc,complex_of_real_add RS sym,
    1.34 -                                      complex_add_mult_distrib]));
    1.35 +                                      left_distrib]));
    1.36  qed_spec_mp "sumc_interval_const";
    1.37  
    1.38  Goal "(ALL n. m <= n --> f n = r) & m <= na \
    1.39 @@ -117,7 +117,7 @@
    1.40  by (induct_tac "na" 1);
    1.41  by (auto_tac (claset(),simpset() addsimps [left_distrib, Suc_diff_n,
    1.42                                        real_of_nat_Suc,complex_of_real_add RS sym,
    1.43 -                                      complex_add_mult_distrib]));
    1.44 +                                      left_distrib]));
    1.45  qed_spec_mp "sumc_interval_const2";
    1.46  
    1.47  (***