# HG changeset patch
# User avigad
# Date 1121786649 -7200
# Node ID 7cb4bcfa058e325720731868352c285992f615fd
# Parent  b24c067b32d671b0768c2c642b3f2b773d3ad3f1
added list of theorem changes to NEWS
added real_of_int_abs to RealDef.thy

diff -r b24c067b32d6 -r 7cb4bcfa058e NEWS
--- a/NEWS	Tue Jul 19 17:21:59 2005 +0200
+++ b/NEWS	Tue Jul 19 17:24:09 2005 +0200
@@ -351,6 +351,41 @@
 
 * Classical reasoning: the meson method now accepts theorems as arguments.
 
+* Introduced various additions and improvements in OrderedGroup.thy and 
+Ring_and_Field.thy, to faciliate calculations involving equalities 
+and inequalities.
+
+* Added rules for simplifying exponents to Parity.thy
+
+Below are some theorems that have been eliminated or modified in this release:
+
+  abs_eq             now named abs_of_nonneg
+  abs_of_ge_0        now named abs_of_nonneg 
+  abs_minus_eq       now named abs_of_nonpos  
+  imp_abs_id         now named abs_of_nonneg
+  imp_abs_neg_id     now named abs_of_nonpos
+  mult_pos           now named mult_pos_pos
+  mult_pos_le        now named mult_nonneg_nonneg
+  mult_pos_neg_le    now named mult_nonneg_nonpos
+  mult_pos_neg2_le   now named mult_nonneg_nonpos2
+  mult_neg           now named mult_neg_neg
+  mult_neg_le        now named mult_nonpos_nonpos
+
+
+*** HOL-Complex ***
+
+* Introduced better support for embedding natural numbers and integers
+in the reals, in RealDef.thy.
+
+* Expanded support for floor and ceiling functions, in RComplete.thy.
+
+Below are some theorems that have been eliminated or modified in this release:
+
+  real_of_int_add    reversed direction of equality (use "THEN sym")
+  real_of_int_minus  reversed direction of equality (use "THEN sym")
+  real_of_int_diff   reversed direction of equality (use "THEN sym")
+  real_of_int_mult   reversed direction of equality (use "THEN sym")
+
 
 *** HOLCF ***
 
diff -r b24c067b32d6 -r 7cb4bcfa058e src/HOL/Real/RealDef.thy
--- a/src/HOL/Real/RealDef.thy	Tue Jul 19 17:21:59 2005 +0200
+++ b/src/HOL/Real/RealDef.thy	Tue Jul 19 17:24:09 2005 +0200
@@ -701,6 +701,9 @@
 lemma real_of_int_le_zero_cancel_iff [simp]: "(real (n::int) <= 0) = (n <= 0)"
 by (simp add: real_of_int_def)
 
+lemma real_of_int_abs [simp]: "real (abs x) = abs(real (x::int))"
+by (auto simp add: abs_if)
+
 lemma int_less_real_le: "((n::int) < m) = (real n + 1 <= real m)"
   apply (subgoal_tac "real n + 1 = real (n + 1)")
   apply (simp del: real_of_int_add)