diff -r dc5e984dfe13 -r f0c3da8477e9 src/HOL/Real/RealOrd.ML
--- a/src/HOL/Real/RealOrd.ML	Tue Dec 19 15:06:14 2000 +0100
+++ b/src/HOL/Real/RealOrd.ML	Tue Dec 19 15:06:59 2000 +0100
@@ -270,7 +270,8 @@
 by (simp_tac (simpset() addsimps [real_add_assoc]) 1);
 qed "real_add_minus_positive_less_self";
 
-Goal "((r::real) <= s) = (-s <= -r)";
+Goal "(-s <= -r) = ((r::real) <= s)";
+by (rtac sym 1);
 by (Step_tac 1);
 by (dres_inst_tac [("x","-s")] real_add_left_le_mono1 1);
 by (dres_inst_tac [("x","r")] real_add_left_le_mono1 2);
@@ -279,7 +280,7 @@
 by (dres_inst_tac [("z","s")] real_add_le_mono1 2);
 by (auto_tac (claset(), simpset() addsimps [real_add_assoc]));
 qed "real_le_minus_iff";
-Addsimps [real_le_minus_iff RS sym];
+Addsimps [real_le_minus_iff];
           
 Goal "0 <= 1r";
 by (rtac (real_zero_less_one RS real_less_imp_le) 1);