| changeset 14308 | c0489217deb2 |
| parent 14305 | f17ca9f6dc8c |
| child 14311 | efda5615bb7d |
--- a/src/HOL/Real/real_arith.ML Sun Dec 21 18:39:27 2003 +0100 +++ b/src/HOL/Real/real_arith.ML Mon Dec 22 12:50:01 2003 +0100 @@ -9,8 +9,7 @@ (** Misc ML bindings **) -val real_inverse_less_iff = thm"real_inverse_less_iff"; -val real_inverse_le_iff = thm"real_inverse_le_iff"; +val inverse_less_iff_less = thm"inverse_less_iff_less"; val pos_real_less_divide_eq = thm"pos_less_divide_eq"; val pos_real_divide_less_eq = thm"pos_divide_less_eq";