diff -r c55a12162944 -r ec91a90c604e src/HOL/Real/RComplete.thy
--- a/src/HOL/Real/RComplete.thy	Wed Oct 06 13:59:33 2004 +0200
+++ b/src/HOL/Real/RComplete.thy	Thu Oct 07 15:42:30 2004 +0200
@@ -153,7 +153,7 @@
 apply (rule lemma_real_complete2b)
 apply (erule_tac [2] order_less_imp_le)
 apply (blast intro!: isLubD2, blast) 
-apply (simp (no_asm_use) add: real_add_assoc)
+apply (simp (no_asm_use) add: add_assoc)
 apply (blast dest: isUbD intro!: setleI [THEN isUbI] intro: add_right_mono)
 apply (blast dest: isUbD intro!: setleI [THEN isUbI] intro: add_right_mono, auto)
 done
@@ -169,7 +169,7 @@
 apply (drule_tac x = n in spec)
 apply (drule_tac c = "real (Suc n)"  in mult_right_mono)
 apply (rule real_of_nat_ge_zero)
-apply (simp add: real_of_nat_Suc_gt_zero [THEN real_not_refl2, THEN not_sym] real_mult_commute)
+apply (simp add: times_divide_eq_right real_of_nat_Suc_gt_zero [THEN real_not_refl2, THEN not_sym] mult_commute)
 apply (subgoal_tac "isUb (UNIV::real set) {z. \<exists>n. z = x* (real (Suc n))} 1")
 apply (subgoal_tac "\<exists>X. X \<in> {z. \<exists>n. z = x* (real (Suc n))}")
 apply (drule reals_complete)