src/HOL/Complex/CStar.ML
changeset 14378 69c4d5997669
parent 14377 f454b3004f8f
     1.1 --- a/src/HOL/Complex/CStar.ML	Thu Feb 05 10:45:28 2004 +0100
     1.2 +++ b/src/HOL/Complex/CStar.ML	Tue Feb 10 12:02:11 2004 +0100
     1.3 @@ -404,10 +404,9 @@
     1.4  Goal "( *fcNat* (%n. z ^ n)) N = (hcomplex_of_complex z) hcpow N";
     1.5  *)
     1.6  
     1.7 -Goalw [hypnat_of_nat_def] 
     1.8 -   "( *fc* (%z. z ^ n)) Z = Z hcpow hypnat_of_nat n";
     1.9 +Goal "( *fc* (%z. z ^ n)) Z = Z hcpow hypnat_of_nat n";
    1.10  by (res_inst_tac [("z","Z")] eq_Abs_hcomplex 1);
    1.11 -by (auto_tac (claset(), simpset() addsimps [hcpow,starfunC]));
    1.12 +by (auto_tac (claset(), simpset() addsimps [hcpow,starfunC,hypnat_of_nat_eq]));
    1.13  qed "starfunC_hcpow";
    1.14  
    1.15  Goal "( *fc* (%h. f (x + h))) xa  = ( *fc* f) (hcomplex_of_complex  x + xa)";