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.24 +    complex_Re/Im_add      ~>  plus_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
    1.41 +    complex_add_def
    1.42 +    complex_minus_def
    1.43 +    complex_diff_def
    1.44 +    complex_one_def
    1.45 +    complex_mult_def
    1.46 +    complex_inverse_def
    1.47 +    complex_scaleR_def
    1.48 +
    1.49  * Removed solvers remote_cvc3 and remote_z3. Use cvc3 and z3 instead.
    1.50  
    1.51  * Nitpick: