src/HOL/Complex/CStar.ML
changeset 14377 f454b3004f8f
parent 14370 b0064703967b
child 14378 69c4d5997669
     1.1 --- a/src/HOL/Complex/CStar.ML	Thu Feb 05 04:30:38 2004 +0100
     1.2 +++ b/src/HOL/Complex/CStar.ML	Thu Feb 05 10:45:28 2004 +0100
     1.3 @@ -194,7 +194,7 @@
     1.4  
     1.5  Goalw [congruent_def] 
     1.6        "congruent hcomplexrel (%X. hcomplexrel``{%n. f (X n)})";
     1.7 -by (safe_tac (claset()));
     1.8 +by (auto_tac (clasimpset() addIffs [hcomplexrel_iff]));
     1.9  by (ALLGOALS(Ultra_tac));
    1.10  qed "starfunC_congruent";
    1.11  
    1.12 @@ -203,7 +203,7 @@
    1.13        "( *fc* f) (Abs_hcomplex(hcomplexrel``{%n. X n})) = \
    1.14  \      Abs_hcomplex(hcomplexrel `` {%n. f (X n)})";
    1.15  by (res_inst_tac [("f","Abs_hcomplex")] arg_cong 1);
    1.16 -by Auto_tac;
    1.17 +by (auto_tac (clasimpset() addIffs [hcomplexrel_iff]));
    1.18  by (Ultra_tac 1);
    1.19  qed "starfunC";
    1.20  
    1.21 @@ -219,7 +219,7 @@
    1.22        "( *fcR* f) (Abs_hcomplex(hcomplexrel``{%n. X n})) = \
    1.23  \      Abs_hypreal(hyprel `` {%n. f (X n)})";
    1.24  by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1);
    1.25 -by Auto_tac;
    1.26 +by (auto_tac (clasimpset() addIffs [hcomplexrel_iff]));
    1.27  by (Ultra_tac 1);
    1.28  qed "starfunCR";
    1.29  
    1.30 @@ -523,7 +523,7 @@
    1.31  
    1.32  Goalw [congruent_def] 
    1.33        "congruent hcomplexrel (%X. hcomplexrel``{%n. f n (X n)})";
    1.34 -by (safe_tac (claset()));
    1.35 +by (auto_tac (clasimpset() addIffs [hcomplexrel_iff]));
    1.36  by (ALLGOALS(Fuf_tac));
    1.37  qed "starfunC_n_congruent";
    1.38  
    1.39 @@ -531,7 +531,7 @@
    1.40       "( *fcn* f) (Abs_hcomplex(hcomplexrel``{%n. X n})) = \
    1.41  \     Abs_hcomplex(hcomplexrel `` {%n. f n (X n)})";
    1.42  by (res_inst_tac [("f","Abs_hcomplex")] arg_cong 1);
    1.43 -by Auto_tac;
    1.44 +by (auto_tac (clasimpset() addIffs [hcomplexrel_iff]));
    1.45  by (Ultra_tac 1);
    1.46  qed "starfunC_n";
    1.47