--- a/src/HOL/Real/real_arith.ML Fri Mar 19 10:48:22 2004 +0100
+++ b/src/HOL/Real/real_arith.ML Fri Mar 19 10:50:06 2004 +0100
@@ -34,7 +34,6 @@
val real_add_commute = thm"real_add_commute";
val real_add_assoc = thm"real_add_assoc";
val real_add_zero_left = thm"real_add_zero_left";
-val real_add_zero_right = thm"real_add_zero_right";
val real_mult = thm"real_mult";
val real_mult_commute = thm"real_mult_commute";
@@ -54,7 +53,6 @@
val real_le_refl = thm"real_le_refl";
val real_le_linear = thm"real_le_linear";
val real_le_trans = thm"real_le_trans";
-val real_le_anti_sym = thm"real_le_anti_sym";
val real_less_le = thm"real_less_le";
val real_less_sum_gt_zero = thm"real_less_sum_gt_zero";
val real_gt_zero_preal_Ex = thm "real_gt_zero_preal_Ex";
@@ -64,7 +62,6 @@
val real_less_all_real2 = thm "real_less_all_real2";
val real_of_preal_le_iff = thm "real_of_preal_le_iff";
val real_mult_order = thm "real_mult_order";
-val real_zero_less_one = thm "real_zero_less_one";
val real_add_less_le_mono = thm "real_add_less_le_mono";
val real_add_le_less_mono = thm "real_add_le_less_mono";
val real_add_order = thm "real_add_order";