--- a/src/HOL/Real/RComplete.thy Sat Feb 19 18:44:34 2005 +0100
+++ b/src/HOL/Real/RComplete.thy Mon Feb 21 15:04:10 2005 +0100
@@ -389,7 +389,7 @@
lemma floor_eq3: "[| real n < x; x < real (Suc n) |] ==> nat(floor x) = n"
apply (rule inj_int [THEN injD])
apply (simp add: real_of_nat_Suc)
-apply (simp add: real_of_nat_Suc floor_eq floor_eq [where n = "of_nat n"])
+apply (simp add: real_of_nat_Suc floor_eq floor_eq [where n = "int n"])
done
lemma floor_eq4: "[| real n \<le> x; x < real (Suc n) |] ==> nat(floor x) = n"
@@ -532,7 +532,3 @@
end
-
-
-
-