diff -r cb3612cc41a3 -r fc075ae929e4 src/HOL/Hyperreal/Transcendental.thy
--- a/src/HOL/Hyperreal/Transcendental.thy	Sun Jan 30 20:48:50 2005 +0100
+++ b/src/HOL/Hyperreal/Transcendental.thy	Tue Feb 01 18:01:57 2005 +0100
@@ -138,8 +138,7 @@
 lemma real_pow_sqrt_eq_sqrt_pow: 
       "0 \<le> x ==> (sqrt x)\<twosuperior> = sqrt(x\<twosuperior>)"
 apply (simp add: sqrt_def)
-apply (subst numeral_2_eq_2)
-apply (auto intro: real_root_pow_pos2 [THEN ssubst] real_root_pos2 [THEN ssubst] simp del: realpow_Suc)
+apply (simp only: numeral_2_eq_2 real_root_pow_pos2 real_root_pos2)
 done
 
 lemma real_pow_sqrt_eq_sqrt_abs_pow2:
@@ -1424,7 +1423,9 @@
 apply (drule sums_minus)
 apply (rule neg_less_iff_less [THEN iffD1]) 
 apply (frule sums_unique, auto simp add: times_divide_eq)
-apply (rule_tac y = "sumr 0 (Suc (Suc (Suc 0))) (%n. - ((- 1) ^ n / (real (fact (2 * n))) * 2 ^ (2 * n)))" in order_less_trans)
+apply (rule_tac y = "sumr 0 (Suc (Suc (Suc 0))) 
+                      (%n. - ((- 1) ^ n / (real(fact (2*n))) * 2 ^ (2*n)))" 
+       in order_less_trans)
 apply (simp (no_asm) add: fact_num_eq_if realpow_num_eq_if del: fact_Suc realpow_Suc)
 apply (simp (no_asm) add: mult_assoc times_divide_eq del: sumr_Suc)
 apply (rule sumr_pos_lt_pair)
@@ -1435,12 +1436,11 @@
 apply (rule real_of_nat_fact_gt_zero)+
 apply (simp (no_asm) add: mult_assoc [symmetric] del: fact_Suc)
 apply (subst fact_lemma) 
-apply (subst fact_Suc)
-apply (subst real_of_nat_mult)
-apply (erule ssubst, subst real_of_nat_mult)
+apply (subst fact_Suc [of "Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))"])
+apply (simp only: real_of_nat_mult)
 apply (rule real_mult_less_mono, force)
-prefer 2 apply force
-apply (rule_tac [2] real_of_nat_fact_gt_zero)
+  apply (rule_tac [3] real_of_nat_fact_gt_zero)
+ prefer 2 apply force
 apply (rule real_of_nat_less_iff [THEN iffD2])
 apply (rule fact_less_mono, auto)
 done