# HG changeset patch
# User paulson
# Date 1072093801 -3600
# Node ID c0489217deb2d44d20860f753aaac6746dfff3ff
# Parent  1cbc24648cf71f555cadf7ed85f91436bd847b33
removing obsolete bindings

diff -r 1cbc24648cf7 -r c0489217deb2 src/HOL/Real/RealArith.thy
--- 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
diff -r 1cbc24648cf7 -r c0489217deb2 src/HOL/Real/RealOrd.thy
--- 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)
diff -r 1cbc24648cf7 -r c0489217deb2 src/HOL/Real/real_arith.ML
--- 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";