overdue NEWS concerning c4daa97ac57a
authorimmler
Tue Jul 01 17:16:11 2014 +0200 (2014-07-01)
changeset 57476dc542b78ef0f
parent 57475 d328664394ab
child 57477 c3b5cb53ea79
overdue NEWS concerning c4daa97ac57a
NEWS
     1.1 --- a/NEWS	Tue Jul 01 16:09:51 2014 +0100
     1.2 +++ b/NEWS	Tue Jul 01 17:16:11 2014 +0200
     1.3 @@ -762,6 +762,62 @@
     1.4      INCOMPATIBILITY: use box instead of greaterThanLessThan or
     1.5      explicit set-comprehensions with eucl_less for other (half-)open
     1.6      intervals.
     1.7 +  - removed dependencies on type class ordered_euclidean_space with
     1.8 +    introduction of "cbox" on euclidean_space
     1.9 +    - renamed theorems:
    1.10 +        interval ~> box
    1.11 +        mem_interval ~> mem_box
    1.12 +        interval_eq_empty ~> box_eq_empty
    1.13 +        interval_ne_empty ~> box_ne_empty
    1.14 +        interval_sing(1) ~> cbox_sing
    1.15 +        interval_sing(2) ~> box_sing
    1.16 +        subset_interval_imp ~> subset_box_imp
    1.17 +        subset_interval ~> subset_box
    1.18 +        open_interval ~> open_box
    1.19 +        closed_interval ~> closed_cbox
    1.20 +        interior_closed_interval ~> interior_cbox
    1.21 +        bounded_closed_interval ~> bounded_cbox
    1.22 +        compact_interval ~> compact_cbox
    1.23 +        bounded_subset_closed_interval_symmetric ~> bounded_subset_cbox_symmetric
    1.24 +        bounded_subset_closed_interval ~> bounded_subset_cbox
    1.25 +        mem_interval_componentwiseI ~> mem_box_componentwiseI
    1.26 +        convex_box ~> convex_prod
    1.27 +        rel_interior_real_interval ~> rel_interior_real_box
    1.28 +        convex_interval ~> convex_box
    1.29 +        convex_hull_eq_real_interval ~> convex_hull_eq_real_cbox
    1.30 +        frechet_derivative_within_closed_interval ~> frechet_derivative_within_cbox
    1.31 +        content_closed_interval' ~> content_cbox'
    1.32 +        elementary_subset_interval ~> elementary_subset_box
    1.33 +        diameter_closed_interval ~> diameter_cbox
    1.34 +        frontier_closed_interval ~> frontier_cbox
    1.35 +        frontier_open_interval ~> frontier_box
    1.36 +        bounded_subset_open_interval_symmetric ~> bounded_subset_box_symmetric
    1.37 +        closure_open_interval ~> closure_box
    1.38 +        open_closed_interval_convex ~> open_cbox_convex
    1.39 +        open_interval_midpoint ~> box_midpoint
    1.40 +        content_image_affinity_interval ~> content_image_affinity_cbox
    1.41 +        is_interval_interval ~> is_interval_cbox + is_interval_box + is_interval_closed_interval
    1.42 +        bounded_interval ~> bounded_closed_interval + bounded_boxes
    1.43 +
    1.44 +    - respective theorems for intervals over the reals:
    1.45 +        content_closed_interval + content_cbox
    1.46 +        has_integral + has_integral_real
    1.47 +        fine_division_exists + fine_division_exists_real
    1.48 +        has_integral_null + has_integral_null_real
    1.49 +        tagged_division_union_interval + tagged_division_union_interval_real
    1.50 +        has_integral_const + has_integral_const_real
    1.51 +        integral_const + integral_const_real
    1.52 +        has_integral_bound + has_integral_bound_real
    1.53 +        integrable_continuous + integrable_continuous_real
    1.54 +        integrable_subinterval + integrable_subinterval_real
    1.55 +        has_integral_reflect_lemma + has_integral_reflect_lemma_real
    1.56 +        integrable_reflect + integrable_reflect_real
    1.57 +        integral_reflect + integral_reflect_real
    1.58 +        image_affinity_interval + image_affinity_cbox
    1.59 +        image_smult_interval + image_smult_cbox
    1.60 +        integrable_const + integrable_const_ivl
    1.61 +        integrable_on_subinterval + integrable_on_subcbox
    1.62 +
    1.63    - renamed theorems:
    1.64      derivative_linear         ~>  has_derivative_bounded_linear
    1.65      derivative_is_linear      ~>  has_derivative_linear