src/HOL/Complex/CLim.ML

        simpset() addsimps [starfunC_lambda_cancel, lemma_nscderiv1,
        hcomplex_of_complex_zero]));
 by (simp_tac (simpset() addsimps [hcomplex_add_divide_distrib]) 1); 
 by (REPEAT(dtac (bex_CInfinitesimal_iff2 RS iffD2) 1));
 by (auto_tac (claset(),
-        simpset() delsimps [hcomplex_times_divide1_eq]
-		  addsimps [hcomplex_times_divide1_eq RS sym]));
+        simpset() delsimps [times_divide_eq_right]
+		  addsimps [times_divide_eq_right RS sym]));
 by (rewtac hcomplex_diff_def);
 by (dres_inst_tac [("D","Db")] lemma_nscderiv2 1);
 by (dtac (capprox_minus_iff RS iffD2 RS (bex_CInfinitesimal_iff2 RS iffD2)) 4);
 by (auto_tac (claset() addSIs [capprox_add_mono1],
       simpset() addsimps [hcomplex_add_mult_distrib, hcomplex_add_mult_distrib2, 

 (*used once, in NSCDERIV_inverse*)
 Goal "[| h: CInfinitesimal; x ~= 0 |] ==> hcomplex_of_complex x + h ~= 0";
 by Auto_tac;  
 qed "CInfinitesimal_add_not_zero";
 
-(***
-Goal "[|(x::hcomplex) ~= 0;  y ~= 0 |]  \
-\     ==> inverse(x) + inverse(y) = (x + y)*inverse(x*y)";
-by (asm_full_simp_tac (simpset() addsimps [hcomplex_inverse_distrib,
-                    hcomplex_add_mult_distrib,hcomplex_mult_assoc RS sym]) 1);
-qed "hcomplex_inverse_add";
-***)
-
 (*Can't get rid of x ~= 0 because it isn't continuous at zero*)
 
 Goalw [nscderiv_def]
      "x ~= 0 ==> NSCDERIV (%x. inverse(x)) x :> (- (inverse x ^ 2))";
 by (rtac ballI 1 THEN Asm_full_simp_tac 1 THEN Step_tac 1);

      simpset() addsimps [starfunC_inverse_inverse,hcomplex_diff_def] 
                delsimps [hcomplex_minus_mult_eq1 RS sym,
                          hcomplex_minus_mult_eq2 RS sym]));
 by (asm_simp_tac
      (simpset() addsimps [hcomplex_inverse_add,
-          hcomplex_inverse_distrib RS sym, hcomplex_minus_inverse RS sym] 
+          inverse_mult_distrib RS sym, hcomplex_minus_inverse RS sym] 
           @ hcomplex_add_ac @ hcomplex_mult_ac 
-       delsimps [hcomplex_minus_mult_eq1 RS sym,
+       delsimps [thm"Ring_and_Field.inverse_minus_eq",
+		 inverse_mult_distrib, hcomplex_minus_mult_eq1 RS sym,
                  hcomplex_minus_mult_eq2 RS sym] ) 1);
 by (asm_simp_tac (simpset() addsimps [hcomplex_mult_assoc RS sym,
                                       hcomplex_add_mult_distrib2] 
          delsimps [hcomplex_minus_mult_eq1 RS sym, 
                    hcomplex_minus_mult_eq2 RS sym]) 1);