diff -r d3f9abe00712 -r b2a894562b8f src/HOL/Real/RealDef.thy
--- a/src/HOL/Real/RealDef.thy	Mon Aug 01 19:20:25 2005 +0200
+++ b/src/HOL/Real/RealDef.thy	Mon Aug 01 19:20:26 2005 +0200
@@ -425,9 +425,9 @@
                  linorder_not_le [where 'a = preal] 
                   real_zero_def real_le real_mult)
   --{*Reduce to the (simpler) @{text "\<le>"} relation *}
-apply (auto  dest!: less_add_left_Ex 
+apply (auto dest!: less_add_left_Ex
      simp add: preal_add_ac preal_mult_ac 
-          preal_add_mult_distrib2 preal_cancels preal_self_less_add_right)
+          preal_add_mult_distrib2 preal_cancels preal_self_less_add_left)
 done
 
 lemma real_mult_less_mono2: "[| (0::real) < z; x < y |] ==> z * x < z * y"
@@ -478,7 +478,6 @@
 apply (auto simp add: real_minus preal_add_ac)
 apply (cut_tac x = x and y = y in linorder_less_linear)
 apply (auto dest!: less_add_left_Ex simp add: preal_add_assoc [symmetric])
-apply (auto simp add: preal_add_commute)
 done
 
 lemma real_of_preal_leD: