NEWS
 changeset 56889 48a745e1bde7 parent 56879 ee2b61f37ad9 child 56901 2f73ef9eb272
```     1.1 --- a/NEWS	Tue May 06 23:35:24 2014 +0200
1.2 +++ b/NEWS	Wed May 07 12:25:35 2014 +0200
1.3 @@ -590,6 +590,48 @@
1.4  * Include more theorems in continuous_intros. Remove the continuous_on_intros,
1.5    isCont_intros collections, these facts are now in continuous_intros.
1.6
1.7 +* Theorems about complex numbers are now stated only using Re and Im, the Complex
1.8 +  constructor is not used anymore. It is possible to use primcorec to defined the
1.9 +  behaviour of a complex-valued function.
1.10 +
1.11 +  Removed theorems about the Complex constructor from the simpset, they are
1.12 +  available as the lemma collection legacy_Complex_simps. This especially
1.13 +  removes
1.14 +    i_complex_of_real: "ii * complex_of_real r = Complex 0 r".
1.15 +
1.16 +  Instead the reverse direction is supported with
1.17 +    Complex_eq: "Complex a b = a + \<i> * b"
1.18 +
1.19 +  Moved csqrt from Fundamental_Algebra_Theorem to Complex.
1.20 +
1.21 +  Renamings:
1.22 +    Re/Im                  ~>  complex.sel
1.23 +    complex_Re/Im_zero     ~>  zero_complex.sel
1.25 +    complex_Re/Im_minus    ~>  uminus_complex.sel
1.26 +    complex_Re/Im_diff     ~>  minus_complex.sel
1.27 +    complex_Re/Im_one      ~>  one_complex.sel
1.28 +    complex_Re/Im_mult     ~>  times_complex.sel
1.29 +    complex_Re/Im_inverse  ~>  inverse_complex.sel
1.30 +    complex_Re/Im_scaleR   ~>  scaleR_complex.sel
1.31 +    complex_Re/Im_i        ~>  ii.sel
1.32 +    complex_Re/Im_cnj      ~>  cnj.sel
1.33 +    Re/Im_cis              ~>  cis.sel
1.34 +
1.35 +    complex_divide_def   ~>  divide_complex_def
1.36 +    complex_norm_def     ~>  norm_complex_def
1.37 +    cmod_def             ~>  norm_complex_de
1.38 +
1.39 +  Removed theorems:
1.40 +    complex_zero_def