1.1 --- a/NEWS	Fri Apr 20 11:14:39 2012 +0200
     1.2 +++ b/NEWS	Fri Apr 20 11:17:01 2012 +0200
     1.3 @@ -479,12 +479,69 @@
     1.4  
     1.5  * Theory HOL/Library/Float: Floating point numbers are now defined as a
     1.6  subset of the real numbers. All operations are defined using the
     1.7 -lifing-framework and most proofs use the transfer method.
     1.8 +lifing-framework and proofs use the transfer method.
     1.9  INCOMPATIBILITY.
    1.10  
    1.11    Changed Operations:
    1.12 -  scale   ~>   exponent
    1.13 -  pow2 x  ~>   use "2 powr (real x)"
    1.14 +  float_abs -> abs
    1.15 +  float_nprt -> nprt
    1.16 +  float_pprt -> pprt
    1.17 +  pow2 -> use powr
    1.18 +  round_down -> float_round_down
    1.19 +  round_up -> float_round_up
    1.20 +  scale -> exponent
    1.21 +
    1.22 +  Removed Operations:
    1.23 +  ceiling_fl, lb_mult, lb_mod, ub_mult, ub_mod
    1.24 +
    1.25 +  Renamed Lemmas:
    1.26 +  abs_float_def -> Float.compute_float_abs
    1.27 +  bitlen_ge0 -> bitlen_nonneg
    1.28 +  bitlen.simps -> Float.compute_bitlen
    1.29 +  float_components -> Float_mantissa_exponent
    1.30 +  float_divl.simps -> Float.compute_float_divl
    1.31 +  float_divr.simps -> Float.compute_float_divr
    1.32 +  float_eq_odd -> mult_powr_eq_mult_powr_iff
    1.33 +  float_power -> real_of_float_power
    1.34 +  lapprox_posrat_def -> Float.compute_lapprox_posrat
    1.35 +  lapprox_rat.simps -> Float.compute_lapprox_rat
    1.36 +  le_float_def' -> Float.compute_float_le
    1.37 +  le_float_def -> less_eq_float.rep_eq
    1.38 +  less_float_def' -> Float.compute_float_less
    1.39 +  less_float_def -> less_float.rep_eq
    1.40 +  normfloat_def -> Float.compute_normfloat
    1.41 +  normfloat_imp_odd_or_zero -> mantissa_not_dvd and mantissa_noteq_0
    1.42 +  normfloat -> normfloat_def
    1.43 +  normfloat_unique -> use normfloat_def
    1.44 +  number_of_float_Float -> Float.compute_float_numeral, Float.compute_float_neg_numeral
    1.45 +  one_float_def -> Float.compute_float_one
    1.46 +  plus_float_def -> Float.compute_float_plus
    1.47 +  rapprox_posrat_def -> Float.compute_rapprox_posrat
    1.48 +  rapprox_rat.simps -> Float.compute_rapprox_rat
    1.49 +  real_of_float_0 -> zero_float.rep_eq
    1.50 +  real_of_float_1 -> one_float.rep_eq
    1.51 +  real_of_float_abs -> abs_float.rep_eq
    1.52 +  real_of_float_add -> plus_float.rep_eq
    1.53 +  real_of_float_minus -> uminus_float.rep_eq
    1.54 +  real_of_float_mult -> times_float.rep_eq
    1.55 +  real_of_float_simp -> Float.rep_eq
    1.56 +  real_of_float_sub -> minus_float.rep_eq
    1.57 +  round_down.simps -> Float.compute_float_round_down
    1.58 +  round_up.simps -> Float.compute_float_round_up
    1.59 +  times_float_def -> Float.compute_float_times
    1.60 +  uminus_float_def -> Float.compute_float_uminus
    1.61 +  zero_float_def -> Float.compute_float_zero
    1.62 +
    1.63 +  Lemmas not necessary anymore, use the transfer method:
    1.64 +  bitlen_B0, bitlen_B1, bitlen_ge1, bitlen_Min, bitlen_Pls, float_divl,
    1.65 +  float_divr, float_le_simp, float_less1_mantissa_bound,
    1.66 +  float_less_simp, float_less_zero, float_le_zero,
    1.67 +  float_pos_less1_e_neg, float_pos_m_pos, float_split, float_split2,
    1.68 +  floor_pos_exp, lapprox_posrat, lapprox_posrat_bottom, lapprox_rat,
    1.69 +  lapprox_rat_bottom, normalized_float, rapprox_posrat,
    1.70 +  rapprox_posrat_le1, rapprox_rat, real_of_float_ge0_exp,
    1.71 +  real_of_float_neg_exp, real_of_float_nge0_exp, round_down floor_fl,
    1.72 +  round_up, zero_le_float, zero_less_float
    1.73  
    1.74  * Session HOL-Word: Discontinued many redundant theorems specific to
    1.75  type 'a word. INCOMPATIBILITY, use the corresponding generic theorems