--- a/src/HOL/Real/RealArith.thy Sun Dec 21 18:39:27 2003 +0100
+++ b/src/HOL/Real/RealArith.thy Mon Dec 22 12:50:01 2003 +0100
@@ -47,7 +47,7 @@
Addsimps [symmetric real_diff_def]
*)
-(** Division by 1, -1 **)
+subsubsection{*Division By @{term 1} and @{term "-1"}*}
lemma real_divide_minus1 [simp]: "x/-1 = -(x::real)"
by simp
--- a/src/HOL/Real/RealOrd.thy Sun Dec 21 18:39:27 2003 +0100
+++ b/src/HOL/Real/RealOrd.thy Mon Dec 22 12:50:01 2003 +0100
@@ -370,14 +370,6 @@
"[| 0 < r; r < x |] ==> inverse x < inverse (r::real)"
by (rule Ring_and_Field.less_imp_inverse_less)
-lemma real_inverse_less_iff:
- "[| 0 < r; 0 < x|] ==> (inverse x < inverse (r::real)) = (r < x)"
-by (rule Ring_and_Field.inverse_less_iff_less)
-
-lemma real_inverse_le_iff:
- "[| 0 < r; 0 < x|] ==> (inverse x \<le> inverse r) = (r \<le> (x::real))"
-by (rule Ring_and_Field.inverse_le_iff_le)
-
(*FIXME: remove the [iff], since the general theorem is already [simp]*)
lemma real_mult_is_0 [iff]: "(x*y = 0) = (x = 0 | y = (0::real))"
by (rule Ring_and_Field.mult_eq_0_iff)
--- 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";