src/HOL/Real/real_arith0.ML

--- a/src/HOL/Real/real_arith0.ML	Mon Dec 29 06:49:26 2003 +0100
+++ b/src/HOL/Real/real_arith0.ML	Thu Jan 01 10:06:32 2004 +0100
@@ -6,6 +6,11 @@
 Instantiation of the generic linear arithmetic package for type real.
 *)
 
+val add_zero_left = thm"Ring_and_Field.add_0";
+val add_zero_right = thm"Ring_and_Field.add_0_right";
+
+val real_mult_left_mono =
+    read_instantiate_sg(sign_of RealBin.thy) [("a","?a::real")] mult_left_mono;
 
 
 local
@@ -17,20 +22,17 @@
      add_real_number_of, minus_real_number_of, diff_real_number_of,
      mult_real_number_of, eq_real_number_of, less_real_number_of,
      le_real_number_of_eq_not_less, real_diff_def,
-     real_minus_add_distrib, real_minus_minus, real_mult_assoc,
-     real_minus_zero,
-     real_add_zero_left, real_add_zero_right,
-     real_add_minus, real_add_minus_left,
-     real_mult_0, real_mult_0_right,
-     real_mult_1, real_mult_1_right,
-     real_mult_minus_eq1, real_mult_minus_eq2];
+     minus_add_distrib, minus_minus, mult_assoc, minus_zero,
+     add_zero_left, add_zero_right, left_minus, right_minus,
+     mult_left_zero, mult_right_zero, mult_1, mult_1_right,
+     minus_mult_left RS sym, minus_mult_right RS sym];
 
 val simprocs = [Real_Times_Assoc.conv, Real_Numeral_Simprocs.combine_numerals]@
                Real_Numeral_Simprocs.cancel_numerals @
                Real_Numeral_Simprocs.eval_numerals;
 
 val mono_ss = simpset() addsimps
-                [real_add_le_mono,real_add_less_mono,
+                [add_mono,add_strict_mono,
                  real_add_less_le_mono,real_add_le_less_mono];
 
 val add_mono_thms_real =
@@ -51,8 +53,8 @@
 val real_mult_mono_thms =
  [(rotate_prems 1 real_mult_less_mono2,
    cvar(real_mult_less_mono2, hd(prems_of real_mult_less_mono2))),
-  (real_mult_le_mono2,
-   cvar(real_mult_le_mono2, hd(tl(prems_of real_mult_le_mono2))))]
+  (real_mult_left_mono,
+   cvar(real_mult_left_mono, hd(tl(prems_of real_mult_left_mono))))]
 
 in