diff -r 2781ac7a4619 -r 27e4d90b35b5 src/HOL/Hyperreal/SEQ.ML
--- a/src/HOL/Hyperreal/SEQ.ML	Fri Jan 05 10:17:19 2001 +0100
+++ b/src/HOL/Hyperreal/SEQ.ML	Fri Jan 05 10:17:48 2001 +0100
@@ -416,15 +416,13 @@
 qed "BseqD";
 
 Goalw [Bseq_def]
-      "[| #0 < K; ALL n. abs(X n) <= K |] \
-\           ==> Bseq X";
+      "[| #0 < K; ALL n. abs(X n) <= K |] ==> Bseq X";
 by (Blast_tac 1);
 qed "BseqI";
 
 Goal "(EX K. #0 < K & (ALL n. abs(X n) <= K)) = \
 \     (EX N. ALL n. abs(X n) <= real_of_nat(Suc N))";
 by Auto_tac;
-by (Force_tac 2); 
 by (cut_inst_tac [("x","K")] reals_Archimedean2 1);
 by (Clarify_tac 1); 
 by (res_inst_tac [("x","n")] exI 1); 
@@ -1255,12 +1253,11 @@
   Proof will use (NS) Cauchy equivalence for convergence and
   also fact that bounded and monotonic sequence converges.  
  ---------------------------------------------------------------*)
-Goalw [Bseq_def] 
-      "[| #0 <= x; x < #1 |] ==> Bseq (%n. x ^ n)";
+Goalw [Bseq_def] "[| #0 <= x; x < #1 |] ==> Bseq (%n. x ^ n)";
 by (res_inst_tac [("x","#1")] exI 1);
-by (auto_tac (claset() addDs [conjI RS realpow_le2] 
+by (auto_tac (claset() addDs [conjI RS realpow_le] 
                        addIs [order_less_imp_le], 
-       simpset() addsimps [real_zero_less_one,abs_eqI1,realpow_abs RS sym] ));
+              simpset() addsimps [abs_eqI1, realpow_abs RS sym] ));
 qed "Bseq_realpow";
 
 Goal "[| #0 <= x; x < #1 |] ==> monoseq (%n. x ^ n)";