NEWS
changeset 36979 da7c06ab3169
parent 36972 aa4bc5a4be1d
child 37020 6c699a8e6927
     1.1 --- a/NEWS	Tue May 18 06:28:42 2010 -0700
     1.2 +++ b/NEWS	Tue May 18 19:00:55 2010 -0700
     1.3 @@ -159,6 +159,41 @@
     1.4  * Dropped normalizing_semiring etc; use the facts in semiring classes
     1.5  instead.  INCOMPATIBILITY.
     1.6  
     1.7 +* Dropped several real-specific versions of lemmas about floor and
     1.8 +ceiling; use the generic lemmas from Archimedean_Field.thy instead.
     1.9 +INCOMPATIBILITY.
    1.10 +
    1.11 +  floor_number_of_eq         ~> floor_number_of
    1.12 +  le_floor_eq_number_of      ~> number_of_le_floor
    1.13 +  le_floor_eq_zero           ~> zero_le_floor
    1.14 +  le_floor_eq_one            ~> one_le_floor
    1.15 +  floor_less_eq_number_of    ~> floor_less_number_of
    1.16 +  floor_less_eq_zero         ~> floor_less_zero
    1.17 +  floor_less_eq_one          ~> floor_less_one
    1.18 +  less_floor_eq_number_of    ~> number_of_less_floor
    1.19 +  less_floor_eq_zero         ~> zero_less_floor
    1.20 +  less_floor_eq_one          ~> one_less_floor
    1.21 +  floor_le_eq_number_of      ~> floor_le_number_of
    1.22 +  floor_le_eq_zero           ~> floor_le_zero
    1.23 +  floor_le_eq_one            ~> floor_le_one
    1.24 +  floor_subtract_number_of   ~> floor_diff_number_of
    1.25 +  floor_subtract_one         ~> floor_diff_one
    1.26 +  ceiling_number_of_eq       ~> ceiling_number_of
    1.27 +  ceiling_le_eq_number_of    ~> ceiling_le_number_of
    1.28 +  ceiling_le_zero_eq         ~> ceiling_le_zero
    1.29 +  ceiling_le_eq_one          ~> ceiling_le_one
    1.30 +  less_ceiling_eq_number_of  ~> number_of_less_ceiling
    1.31 +  less_ceiling_eq_zero       ~> zero_less_ceiling
    1.32 +  less_ceiling_eq_one        ~> one_less_ceiling
    1.33 +  ceiling_less_eq_number_of  ~> ceiling_less_number_of
    1.34 +  ceiling_less_eq_zero       ~> ceiling_less_zero
    1.35 +  ceiling_less_eq_one        ~> ceiling_less_one
    1.36 +  le_ceiling_eq_number_of    ~> number_of_le_ceiling
    1.37 +  le_ceiling_eq_zero         ~> zero_le_ceiling
    1.38 +  le_ceiling_eq_one          ~> one_le_ceiling
    1.39 +  ceiling_subtract_number_of ~> ceiling_diff_number_of
    1.40 +  ceiling_subtract_one       ~> ceiling_diff_one
    1.41 +
    1.42  * Theory 'Finite_Set': various folding_XXX locales facilitate the
    1.43  application of the various fold combinators on finite sets.
    1.44