--- a/src/HOL/Real/RealOrd.thy Tue Dec 23 06:35:41 2003 +0100
+++ b/src/HOL/Real/RealOrd.thy Tue Dec 23 12:54:15 2003 +0100
@@ -316,7 +316,7 @@
by (rule Ring_and_Field.add_le_imp_le_right)
lemma real_le_add_left_cancel: "!!(A::real). C + A \<le> C + B ==> A \<le> B"
- by (rule (*Ring_and_Field.*)add_le_imp_le_left)
+ by (rule Ring_and_Field.add_le_imp_le_left)
lemma real_add_right_cancel_less: "(v+z < w+z) = (v < (w::real))"
by (rule Ring_and_Field.add_less_cancel_right)
--- a/src/HOL/Real/real_arith.ML Tue Dec 23 06:35:41 2003 +0100
+++ b/src/HOL/Real/real_arith.ML Tue Dec 23 12:54:15 2003 +0100
@@ -11,6 +11,15 @@
val inverse_less_iff_less = thm"Ring_and_Field.inverse_less_iff_less";
val add_right_mono = thm"Ring_and_Field.add_right_mono";
+val times_divide_eq_left = thm "times_divide_eq_left";
+val times_divide_eq_right = thm "times_divide_eq_right";
+val inverse_mult_distrib = thm "inverse_mult_distrib";
+val minus_minus = thm "minus_minus";
+val left_inverse = thm "left_inverse";
+val right_inverse = thm "right_inverse";
+val inverse_minus_eq = thm "inverse_minus_eq";
+val minus_mult_left = thm "minus_mult_left";
+val minus_mult_right = thm "minus_mult_right";
val pos_real_less_divide_eq = thm"pos_less_divide_eq";
val pos_real_divide_less_eq = thm"pos_divide_less_eq";