src/HOL/Complex/ComplexArith0.ML

 qed "complex_inverse_eq_divide";
 
 Goal "(inverse(x::complex) = 0) = (x = 0)";
 by (auto_tac (claset(), 
               simpset() addsimps [COMPLEX_INVERSE_ZERO]));  
-by (rtac ccontr 1); 
-by (blast_tac (claset() addDs [complex_inverse_not_zero]) 1); 
 qed "complex_inverse_zero_iff";
 Addsimps [complex_inverse_zero_iff];
 
 Goal "(x/y = 0) = (x=0 | y=(0::complex))";
 by (auto_tac (claset(), simpset() addsimps [complex_divide_def]));  

 qed "complex_add_minus_iff";
 Addsimps [complex_add_minus_iff];
 
 Goal "(-b = -a) = (b = (a::complex))";
 by Auto_tac;
-by (etac ( inj_complex_minus RS injD) 1);
 qed "complex_minus_eq_cancel";
 Addsimps [complex_minus_eq_cancel];
 
 (*Distributive laws for literals*)
 Addsimps (map (inst "w" "number_of ?v")