src/HOL/Complex/NSComplexBin.ML
changeset 14377 f454b3004f8f
parent 14373 67a628beb981
child 14378 69c4d5997669
     1.1 --- a/src/HOL/Complex/NSComplexBin.ML	Thu Feb 05 04:30:38 2004 +0100
     1.2 +++ b/src/HOL/Complex/NSComplexBin.ML	Thu Feb 05 10:45:28 2004 +0100
     1.3 @@ -482,6 +482,7 @@
     1.4  
     1.5  (*** Real and imaginary stuff ***)
     1.6  
     1.7 +(*Convert???
     1.8  Goalw [hcomplex_number_of_def] 
     1.9    "((number_of xa :: hcomplex) + iii * number_of ya = \
    1.10  \       number_of xb + iii * number_of yb) = \
    1.11 @@ -561,6 +562,7 @@
    1.12      hcomplex_hypreal_number_of,hcomplex_of_hypreal_zero_iff]));
    1.13  qed "hcomplex_number_of_eq_cancel_iff3a";
    1.14  Addsimps [hcomplex_number_of_eq_cancel_iff3a];
    1.15 +*)
    1.16  
    1.17  Goalw [hcomplex_number_of_def] "hcnj (number_of v :: hcomplex) = number_of v";
    1.18  by (rtac (hcomplex_hypreal_number_of RS ssubst) 1);