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