src/HOL/Complex/CLim.ML
changeset 14320 fb7a114826be
parent 14318 7dbd3988b15b
child 14323 27724f528f82
     1.1 --- a/src/HOL/Complex/CLim.ML	Tue Dec 23 14:45:23 2003 +0100
     1.2 +++ b/src/HOL/Complex/CLim.ML	Tue Dec 23 14:45:47 2003 +0100
     1.3 @@ -468,12 +468,12 @@
     1.4  by Auto_tac;
     1.5  by (dres_inst_tac [("x","hcomplex_of_complex a + x")] spec 1);
     1.6  by (dres_inst_tac [("x","- hcomplex_of_complex a + x")] spec 2);
     1.7 -by (Step_tac 1);
     1.8 +by Safe_tac;
     1.9  by (Asm_full_simp_tac 1);
    1.10  by (rtac ((mem_cinfmal_iff RS iffD2) RS 
    1.11      (CInfinitesimal_add_capprox_self RS capprox_sym)) 1);
    1.12  by (rtac (capprox_minus_iff2 RS iffD1) 4);
    1.13 -by (asm_full_simp_tac (simpset() addsimps [hcomplex_add_commute]) 3);
    1.14 +by (asm_full_simp_tac (simpset() addsimps compare_rls@[hcomplex_add_commute]) 3);
    1.15  by (res_inst_tac [("z","x")] eq_Abs_hcomplex 2);
    1.16  by (res_inst_tac [("z","x")] eq_Abs_hcomplex 4);
    1.17  by (auto_tac (claset(),
    1.18 @@ -747,7 +747,8 @@
    1.19  by (auto_tac (claset(),simpset() addsimps [isNSContc_NSCLIM_iff,
    1.20      NSCLIM_def,hcomplex_diff_def]));
    1.21  by (dtac (capprox_minus_iff RS iffD1) 1);
    1.22 -by (dtac (CLAIM "x ~= a ==> x + - a ~= (0::hcomplex)") 1);
    1.23 +by (subgoal_tac "xa + - (hcomplex_of_complex x) ~= 0" 1);
    1.24 + by (asm_full_simp_tac (simpset() addsimps compare_rls) 2);
    1.25  by (dres_inst_tac [("x","- hcomplex_of_complex x + xa")] bspec 1);
    1.26  by (asm_full_simp_tac (simpset() addsimps [hcomplex_add_assoc RS sym]) 2);
    1.27  by (auto_tac (claset(),simpset() addsimps 
    1.28 @@ -1041,12 +1042,14 @@
    1.29  by (simp_tac (simpset() addsimps [NSCDERIV_CDERIV_iff]) 1);
    1.30  qed "NSCDERIV_pow";
    1.31  
    1.32 -Goal "\\<lbrakk> CDERIV f x :> D; D = E \\<rbrakk> \\<Longrightarrow> CDERIV f x :> E";
    1.33 +Goal "[|CDERIV f x :> D; D = E|] ==> CDERIV f x :> E";
    1.34  by Auto_tac;
    1.35  qed "lemma_CDERIV_subst";
    1.36  
    1.37  (*used once, in NSCDERIV_inverse*)
    1.38  Goal "[| h: CInfinitesimal; x ~= 0 |] ==> hcomplex_of_complex x + h ~= 0";
    1.39 +by (Clarify_tac 1);
    1.40 +by (dtac (thm"equals_zero_I") 1);
    1.41  by Auto_tac;  
    1.42  qed "CInfinitesimal_add_not_zero";
    1.43  
    1.44 @@ -1062,7 +1065,7 @@
    1.45                 delsimps [hcomplex_minus_mult_eq1 RS sym,
    1.46                           hcomplex_minus_mult_eq2 RS sym]));
    1.47  by (asm_simp_tac
    1.48 -     (simpset() addsimps [hcomplex_inverse_add,
    1.49 +     (simpset() addsimps [inverse_add,
    1.50            inverse_mult_distrib RS sym, hcomplex_minus_inverse RS sym] 
    1.51            @ hcomplex_add_ac @ hcomplex_mult_ac 
    1.52         delsimps [thm"Ring_and_Field.inverse_minus_eq",