added list of theorem changes to NEWS
authoravigad
Tue Jul 19 17:24:09 2005 +0200 (2005-07-19)
changeset 168887cb4bcfa058e
parent 16887 b24c067b32d6
child 16889 b50947fa958d
added list of theorem changes to NEWS
added real_of_int_abs to RealDef.thy
NEWS
src/HOL/Real/RealDef.thy
     1.1 --- a/NEWS	Tue Jul 19 17:21:59 2005 +0200
     1.2 +++ b/NEWS	Tue Jul 19 17:24:09 2005 +0200
     1.3 @@ -351,6 +351,41 @@
     1.4  
     1.5  * Classical reasoning: the meson method now accepts theorems as arguments.
     1.6  
     1.7 +* Introduced various additions and improvements in OrderedGroup.thy and 
     1.8 +Ring_and_Field.thy, to faciliate calculations involving equalities 
     1.9 +and inequalities.
    1.10 +
    1.11 +* Added rules for simplifying exponents to Parity.thy
    1.12 +
    1.13 +Below are some theorems that have been eliminated or modified in this release:
    1.14 +
    1.15 +  abs_eq             now named abs_of_nonneg
    1.16 +  abs_of_ge_0        now named abs_of_nonneg 
    1.17 +  abs_minus_eq       now named abs_of_nonpos  
    1.18 +  imp_abs_id         now named abs_of_nonneg
    1.19 +  imp_abs_neg_id     now named abs_of_nonpos
    1.20 +  mult_pos           now named mult_pos_pos
    1.21 +  mult_pos_le        now named mult_nonneg_nonneg
    1.22 +  mult_pos_neg_le    now named mult_nonneg_nonpos
    1.23 +  mult_pos_neg2_le   now named mult_nonneg_nonpos2
    1.24 +  mult_neg           now named mult_neg_neg
    1.25 +  mult_neg_le        now named mult_nonpos_nonpos
    1.26 +
    1.27 +
    1.28 +*** HOL-Complex ***
    1.29 +
    1.30 +* Introduced better support for embedding natural numbers and integers
    1.31 +in the reals, in RealDef.thy.
    1.32 +
    1.33 +* Expanded support for floor and ceiling functions, in RComplete.thy.
    1.34 +
    1.35 +Below are some theorems that have been eliminated or modified in this release:
    1.36 +
    1.37 +  real_of_int_add    reversed direction of equality (use "THEN sym")
    1.38 +  real_of_int_minus  reversed direction of equality (use "THEN sym")
    1.39 +  real_of_int_diff   reversed direction of equality (use "THEN sym")
    1.40 +  real_of_int_mult   reversed direction of equality (use "THEN sym")
    1.41 +
    1.42  
    1.43  *** HOLCF ***
    1.44  
     2.1 --- a/src/HOL/Real/RealDef.thy	Tue Jul 19 17:21:59 2005 +0200
     2.2 +++ b/src/HOL/Real/RealDef.thy	Tue Jul 19 17:24:09 2005 +0200
     2.3 @@ -701,6 +701,9 @@
     2.4  lemma real_of_int_le_zero_cancel_iff [simp]: "(real (n::int) <= 0) = (n <= 0)"
     2.5  by (simp add: real_of_int_def)
     2.6  
     2.7 +lemma real_of_int_abs [simp]: "real (abs x) = abs(real (x::int))"
     2.8 +by (auto simp add: abs_if)
     2.9 +
    2.10  lemma int_less_real_le: "((n::int) < m) = (real n + 1 <= real m)"
    2.11    apply (subgoal_tac "real n + 1 = real (n + 1)")
    2.12    apply (simp del: real_of_int_add)