# HG changeset patch
# User immler
# Date 1404227771 -7200
# Node ID dc542b78ef0f25333e406ab1db65d907f46f968a
# Parent  d328664394ab5a362689a8b65f8ace1cc226075e
overdue NEWS concerning c4daa97ac57a

diff -r d328664394ab -r dc542b78ef0f NEWS
--- a/NEWS	Tue Jul 01 16:09:51 2014 +0100
+++ b/NEWS	Tue Jul 01 17:16:11 2014 +0200
@@ -762,6 +762,62 @@
     INCOMPATIBILITY: use box instead of greaterThanLessThan or
     explicit set-comprehensions with eucl_less for other (half-)open
     intervals.
+  - removed dependencies on type class ordered_euclidean_space with
+    introduction of "cbox" on euclidean_space
+    - renamed theorems:
+        interval ~> box
+        mem_interval ~> mem_box
+        interval_eq_empty ~> box_eq_empty
+        interval_ne_empty ~> box_ne_empty
+        interval_sing(1) ~> cbox_sing
+        interval_sing(2) ~> box_sing
+        subset_interval_imp ~> subset_box_imp
+        subset_interval ~> subset_box
+        open_interval ~> open_box
+        closed_interval ~> closed_cbox
+        interior_closed_interval ~> interior_cbox
+        bounded_closed_interval ~> bounded_cbox
+        compact_interval ~> compact_cbox
+        bounded_subset_closed_interval_symmetric ~> bounded_subset_cbox_symmetric
+        bounded_subset_closed_interval ~> bounded_subset_cbox
+        mem_interval_componentwiseI ~> mem_box_componentwiseI
+        convex_box ~> convex_prod
+        rel_interior_real_interval ~> rel_interior_real_box
+        convex_interval ~> convex_box
+        convex_hull_eq_real_interval ~> convex_hull_eq_real_cbox
+        frechet_derivative_within_closed_interval ~> frechet_derivative_within_cbox
+        content_closed_interval' ~> content_cbox'
+        elementary_subset_interval ~> elementary_subset_box
+        diameter_closed_interval ~> diameter_cbox
+        frontier_closed_interval ~> frontier_cbox
+        frontier_open_interval ~> frontier_box
+        bounded_subset_open_interval_symmetric ~> bounded_subset_box_symmetric
+        closure_open_interval ~> closure_box
+        open_closed_interval_convex ~> open_cbox_convex
+        open_interval_midpoint ~> box_midpoint
+        content_image_affinity_interval ~> content_image_affinity_cbox
+        is_interval_interval ~> is_interval_cbox + is_interval_box + is_interval_closed_interval
+        bounded_interval ~> bounded_closed_interval + bounded_boxes
+
+    - respective theorems for intervals over the reals:
+        content_closed_interval + content_cbox
+        has_integral + has_integral_real
+        fine_division_exists + fine_division_exists_real
+        has_integral_null + has_integral_null_real
+        tagged_division_union_interval + tagged_division_union_interval_real
+        has_integral_const + has_integral_const_real
+        integral_const + integral_const_real
+        has_integral_bound + has_integral_bound_real
+        integrable_continuous + integrable_continuous_real
+        integrable_subinterval + integrable_subinterval_real
+        has_integral_reflect_lemma + has_integral_reflect_lemma_real
+        integrable_reflect + integrable_reflect_real
+        integral_reflect + integral_reflect_real
+        image_affinity_interval + image_affinity_cbox
+        image_smult_interval + image_smult_cbox
+        integrable_const + integrable_const_ivl
+        integrable_on_subinterval + integrable_on_subcbox
+
   - renamed theorems:
     derivative_linear         ~>  has_derivative_bounded_linear
     derivative_is_linear      ~>  has_derivative_linear