# HG changeset patch
# User wenzelm
# Date 1235659355 -3600
# Node ID 37f47ea6fed190083f7337428278cd12c54947cf
# Parent  b094999e1d334f6b8ae1503aeaed34fa98b1e879# Parent  5c6efec476aea08c7fdd3e81e9d09c514b6f729b
merged

diff -r 5c6efec476ae -r 37f47ea6fed1 src/HOL/Archimedean_Field.thy
--- a/src/HOL/Archimedean_Field.thy	Thu Feb 26 14:16:30 2009 +0100
+++ b/src/HOL/Archimedean_Field.thy	Thu Feb 26 15:42:35 2009 +0100
@@ -391,10 +391,10 @@
 
 subsection {* Negation *}
 
-lemma floor_minus [simp]: "floor (- x) = - ceiling x"
+lemma floor_minus: "floor (- x) = - ceiling x"
   unfolding ceiling_def by simp
 
-lemma ceiling_minus [simp]: "ceiling (- x) = - floor x"
+lemma ceiling_minus: "ceiling (- x) = - floor x"
   unfolding ceiling_def by simp
 
 end
diff -r 5c6efec476ae -r 37f47ea6fed1 src/HOL/Decision_Procs/MIR.thy
--- a/src/HOL/Decision_Procs/MIR.thy	Thu Feb 26 14:16:30 2009 +0100
+++ b/src/HOL/Decision_Procs/MIR.thy	Thu Feb 26 15:42:35 2009 +0100
@@ -5926,7 +5926,7 @@
 apply mir
 done
 
-lemma "ALL x y. \<lfloor>x\<rfloor> = \<lfloor>y\<rfloor> \<longrightarrow> 0 \<le> abs (y - x) \<and> abs (y - x) \<le> 1"
+lemma "ALL (x::real) (y::real). \<lfloor>x\<rfloor> = \<lfloor>y\<rfloor> \<longrightarrow> 0 \<le> abs (y - x) \<and> abs (y - x) \<le> 1"
 apply mir
 done
 
diff -r 5c6efec476ae -r 37f47ea6fed1 src/HOL/RComplete.thy
--- a/src/HOL/RComplete.thy	Thu Feb 26 14:16:30 2009 +0100
+++ b/src/HOL/RComplete.thy	Thu Feb 26 15:42:35 2009 +0100
@@ -501,13 +501,13 @@
 unfolding real_of_nat_def by simp
 
 lemma floor_minus_real_of_nat [simp]: "floor (- real (n::nat)) = - int n"
-unfolding real_of_nat_def by simp
+unfolding real_of_nat_def by (simp add: floor_minus)
 
 lemma floor_real_of_int [simp]: "floor (real (n::int)) = n"
 unfolding real_of_int_def by simp
 
 lemma floor_minus_real_of_int [simp]: "floor (- real (n::int)) = - n"
-unfolding real_of_int_def by simp
+unfolding real_of_int_def by (simp add: floor_minus)
 
 lemma real_lb_ub_int: " \<exists>n::int. real n \<le> r & r < real (n+1)"
 unfolding real_of_int_def by (rule floor_exists)