# HG changeset patch
# User wenzelm
# Date 1121354212 -7200
# Node ID c90a1f450327d99faf8af54a0ae2dd611d112f04
# Parent  ed53f24149f6989043bb28bbf397ab95743c6ed4
accomodate change of real_of_XXX;

diff -r ed53f24149f6 -r c90a1f450327 src/HOL/Real/RComplete.thy
--- a/src/HOL/Real/RComplete.thy	Thu Jul 14 14:05:48 2005 +0200
+++ b/src/HOL/Real/RComplete.thy	Thu Jul 14 17:16:52 2005 +0200
@@ -354,12 +354,6 @@
 apply (insert real_lb_ub_int [of r], safe)
 apply (rule theI2)
 apply auto
-apply (subst int_le_real_less, simp)
-apply (drule_tac x = n in spec)
-apply auto
-apply (subgoal_tac "n <= x")
-apply simp
-apply (subst int_le_real_less, simp)
 done
 
 lemma floor_mono: "x < y ==> floor x \<le> floor y"
@@ -385,7 +379,6 @@
 apply (insert real_lb_ub_int [of x], erule exE)
 apply (rule theI2)
 apply (auto intro: lemma_floor) 
-apply (auto simp add: order_eq_iff int_le_real_less)
 done
 
 lemma floor_eq: "[| real n < x; x < real n + 1 |] ==> floor x = n"
@@ -429,7 +422,6 @@
 apply (insert real_lb_ub_int [of r], safe)
 apply (rule theI2)
 apply (auto intro: lemma_floor)
-apply (auto simp add: order_eq_iff int_le_real_less)
 done
 
 lemma real_of_int_floor_gt_diff_one [simp]: "r - 1 < real(floor r)"
@@ -437,7 +429,6 @@
 apply (insert real_lb_ub_int [of r], safe)
 apply (rule theI2)
 apply (auto intro: lemma_floor)
-apply (auto simp add: order_eq_iff int_le_real_less)
 done
 
 lemma real_of_int_floor_add_one_ge [simp]: "r \<le> real(floor r) + 1"
diff -r ed53f24149f6 -r c90a1f450327 src/HOL/Real/real_arith.ML
--- a/src/HOL/Real/real_arith.ML	Thu Jul 14 14:05:48 2005 +0200
+++ b/src/HOL/Real/real_arith.ML	Thu Jul 14 17:16:52 2005 +0200
@@ -99,9 +99,9 @@
 local
 
 val simps = [real_of_nat_zero, real_of_nat_Suc, real_of_nat_add, 
-       real_of_nat_mult, real_of_int_zero, real_of_one, real_of_int_add RS sym,
-       real_of_int_minus RS sym, real_of_int_diff RS sym,
-       real_of_int_mult RS sym, real_of_int_of_nat_eq,
+       real_of_nat_mult, real_of_int_zero, real_of_one, real_of_int_add,
+       real_of_int_minus, real_of_int_diff,
+       real_of_int_mult, real_of_int_of_nat_eq,
        real_of_nat_number_of, real_number_of];
 
 val int_inj_thms = [real_of_int_le_iff RS iffD2, real_of_int_less_iff RS iffD2,