src/HOL/Complex/NSCA.ML
changeset 14377 f454b3004f8f
parent 14374 61de62096768
child 14387 e96d5c42c4b0
     1.1 --- a/src/HOL/Complex/NSCA.ML	Thu Feb 05 04:30:38 2004 +0100
     1.2 +++ b/src/HOL/Complex/NSCA.ML	Thu Feb 05 10:45:28 2004 +0100
     1.3 @@ -943,11 +943,8 @@
     1.4  \     |] ==> Abs_hcomplex(hcomplexrel ``{%n. X n}) : SComplex";
     1.5  by (auto_tac (claset(),simpset() addsimps [SComplex_def,
     1.6      hcomplex_of_complex_def,SReal_def,hypreal_of_real_def]));
     1.7 -by (res_inst_tac [("x","complex_of_real r + ii  * complex_of_real ra")] exI 1);
     1.8 +by (res_inst_tac [("x","Complex r ra")] exI 1);
     1.9  by (Ultra_tac 1);
    1.10 -by (case_tac "X x" 1);
    1.11 -by (auto_tac (claset(),simpset() addsimps [complex_of_real_def,i_def,
    1.12 -    complex_add,complex_mult]));
    1.13  qed "Reals_Re_Im_SComplex";
    1.14  
    1.15  Goal "(Abs_hcomplex(hcomplexrel ``{%n. X n}) : SComplex) = \
    1.16 @@ -987,8 +984,7 @@
    1.17  by (res_inst_tac [("z","t")] eq_Abs_hypreal 1);
    1.18  by (res_inst_tac [("z","ta")] eq_Abs_hypreal 1);
    1.19  by Auto_tac;
    1.20 -by (res_inst_tac [("x","%n. complex_of_real (xa n) + ii * complex_of_real (xb n)")]
    1.21 -    exI 1);
    1.22 +by (res_inst_tac [("x","%n. Complex (xa n) (xb n)")] exI 1);
    1.23  by Auto_tac;
    1.24  qed "stc_part_Ex";
    1.25