# HG changeset patch
# User paulson
# Date 1072180455 -3600
# Node ID 85125b18d38a5ecb196cf3eda8638ab9d46fb87e
# Parent  91b897b9a2dc06655e7c17e0443d0345edfeb8d5
more ML bindings

diff -r 91b897b9a2dc -r 85125b18d38a src/HOL/Real/RealOrd.thy
--- 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)
diff -r 91b897b9a2dc -r 85125b18d38a src/HOL/Real/real_arith.ML
--- 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";