1.1 --- a/src/HOL/Real/RealDef.thy	Wed Jan 28 10:41:49 2004 +0100
     1.2 +++ b/src/HOL/Real/RealDef.thy	Wed Jan 28 17:01:01 2004 +0100
     1.3 @@ -1017,7 +1017,6 @@
     1.4  lemma real_of_nat_ge_zero_cancel_iff [simp]: "(0 \<le> real (n::nat)) = (0 \<le> n)"
     1.5  by (simp add: linorder_not_less)
     1.6  
     1.7 -text{*Now obsolete, but used in Hyperreal/IntFloor???*}
     1.8  lemma real_of_int_real_of_nat: "real (int n) = real n"
     1.9  by (simp add: real_of_nat_def)
    1.10