1.1 --- a/NEWS	Thu Apr 03 17:16:02 2014 +0200
     1.2 +++ b/NEWS	Thu Apr 03 17:56:08 2014 +0200
     1.3 @@ -534,6 +534,13 @@
     1.4  
     1.5    - Renamed FDERIV_... lemmas to has_derivative_...
     1.6  
     1.7 +  - renamed deriv (the syntax constant used for "DERIV _ _ :> _") to DERIV
     1.8 +
     1.9 +  - removed DERIV_intros, has_derivative_eq_intros
    1.10 +
    1.11 +  - introduced derivative_intros and deriative_eq_intros which includes now rules for
    1.12 +    DERIV, has_derivative and has_vector_derivative.
    1.13 +
    1.14    - Other renamings:
    1.15      differentiable_def        ~>  real_differentiable_def
    1.16      differentiableE           ~>  real_differentiableE
    1.17 @@ -541,6 +548,7 @@
    1.18      field_fderiv_def          ~>  field_has_derivative_at
    1.19      isDiff_der                ~>  differentiable_def
    1.20      deriv_fderiv              ~>  has_field_derivative_def
    1.21 +    deriv_def                 ~>  DERIV_def
    1.22  INCOMPATIBILITY.
    1.23  
    1.24  * Include more theorems in continuous_intros. Remove the continuous_on_intros,