src/HOL/Complex/CStar.ML

 by (Auto_tac);
 qed "starfunCR_n_starfunCR";
 
 Goalw [congruent_def] 
       "congruent hcomplexrel (%X. hcomplexrel``{%n. f (X n)})";
-by (safe_tac (claset()));
+by (auto_tac (clasimpset() addIffs [hcomplexrel_iff]));
 by (ALLGOALS(Ultra_tac));
 qed "starfunC_congruent";
 
 (* f::complex => complex *)
 Goalw [starfunC_def]
       "( *fc* f) (Abs_hcomplex(hcomplexrel``{%n. X n})) = \
 \      Abs_hcomplex(hcomplexrel `` {%n. f (X n)})";
 by (res_inst_tac [("f","Abs_hcomplex")] arg_cong 1);
-by Auto_tac;
+by (auto_tac (clasimpset() addIffs [hcomplexrel_iff]));
 by (Ultra_tac 1);
 qed "starfunC";
 
 Goalw [starfunRC_def]
       "( *fRc* f) (Abs_hypreal(hyprel``{%n. X n})) = \

 
 Goalw [starfunCR_def]
       "( *fcR* f) (Abs_hcomplex(hcomplexrel``{%n. X n})) = \
 \      Abs_hypreal(hyprel `` {%n. f (X n)})";
 by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1);
-by Auto_tac;
+by (auto_tac (clasimpset() addIffs [hcomplexrel_iff]));
 by (Ultra_tac 1);
 qed "starfunCR";
 
 (**  multiplication: ( *f ) x ( *g ) = *(f x g) **)
 

 (* Internal functions - some redundancy with *fc* now                                *)
 (*-----------------------------------------------------------------------------------*)
 
 Goalw [congruent_def] 
       "congruent hcomplexrel (%X. hcomplexrel``{%n. f n (X n)})";
-by (safe_tac (claset()));
+by (auto_tac (clasimpset() addIffs [hcomplexrel_iff]));
 by (ALLGOALS(Fuf_tac));
 qed "starfunC_n_congruent";
 
 Goalw [starfunC_n_def]
      "( *fcn* f) (Abs_hcomplex(hcomplexrel``{%n. X n})) = \
 \     Abs_hcomplex(hcomplexrel `` {%n. f n (X n)})";
 by (res_inst_tac [("f","Abs_hcomplex")] arg_cong 1);
-by Auto_tac;
+by (auto_tac (clasimpset() addIffs [hcomplexrel_iff]));
 by (Ultra_tac 1);
 qed "starfunC_n";
 
 (**  multiplication: ( *fn ) x ( *gn ) = *(fn x gn) **)