--- 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)