1.1 --- a/src/HOL/Hyperreal/IntFloor.ML	Mon Feb 16 15:24:03 2004 +0100
     1.2 +++ b/src/HOL/Hyperreal/IntFloor.ML	Tue Feb 17 10:41:59 2004 +0100
     1.3 @@ -4,8 +4,6 @@
     1.4      Description: Floor and ceiling operations over reals
     1.5  *)
     1.6  
     1.7 -val real_number_of = thm"real_number_of";
     1.8 -
     1.9  Goal "((number_of n) < real (m::int)) = (number_of n < m)";
    1.10  by Auto_tac;
    1.11  by (rtac (real_of_int_less_iff RS iffD1) 1);