src/HOL/Real/RealDef.thy
changeset 14369 c50188fe6366
parent 14365 3d4df8c166ae
child 14378 69c4d5997669
--- a/src/HOL/Real/RealDef.thy	Wed Jan 28 10:41:49 2004 +0100
+++ b/src/HOL/Real/RealDef.thy	Wed Jan 28 17:01:01 2004 +0100
@@ -1017,7 +1017,6 @@
 lemma real_of_nat_ge_zero_cancel_iff [simp]: "(0 \<le> real (n::nat)) = (0 \<le> n)"
 by (simp add: linorder_not_less)
 
-text{*Now obsolete, but used in Hyperreal/IntFloor???*}
 lemma real_of_int_real_of_nat: "real (int n) = real n"
 by (simp add: real_of_nat_def)