diff -r 950c12139016 -r ad66687ece6e src/HOL/Real/RealOrd.thy
--- a/src/HOL/Real/RealOrd.thy	Fri Dec 05 12:58:18 2003 +0100
+++ b/src/HOL/Real/RealOrd.thy	Fri Dec 05 18:10:59 2003 +0100
@@ -565,10 +565,10 @@
 subsection{*Inverse and Division*}
 
 lemma real_inverse_gt_0: "0 < x ==> 0 < inverse (x::real)"
-  by (rule Ring_and_Field.inverse_gt_0)
+  by (rule Ring_and_Field.positive_imp_inverse_positive)
 
 lemma real_inverse_less_0: "x < 0 ==> inverse (x::real) < 0"
-  by (rule Ring_and_Field.inverse_less_0)
+  by (rule Ring_and_Field.negative_imp_inverse_negative)
 
 lemma real_mult_less_cancel1: "[| (0::real) < z; x * z < y * z |] ==> x < y"
 by (force simp add: Ring_and_Field.mult_less_cancel_right