# HG changeset patch
# User paulson
# Date 977421212 -3600
# Node ID 12b16641845558de0204ce60046a2f419be5ba76
# Parent  1ce5a189f672e4fa166340b51d6c3ac36d0a4c19
this makes the proof run (or run faster)

diff -r 1ce5a189f672 -r 12b166418455 src/HOL/Real/Hyperreal/SEQ.ML
--- a/src/HOL/Real/Hyperreal/SEQ.ML	Thu Dec 21 18:08:10 2000 +0100
+++ b/src/HOL/Real/Hyperreal/SEQ.ML	Thu Dec 21 18:53:32 2000 +0100
@@ -1040,6 +1040,7 @@
 by (REPEAT(dtac (HNatInfinite_whn RSN (2,bspec)) 1));
 by (dres_inst_tac [("x","whn")] spec 1);
 by (REPEAT(dtac (bex_Infinitesimal_iff2 RS iffD2) 1));
+by Auto_tac;
 by (auto_tac (claset() addIs 
     [hypreal_of_real_le_add_Infininitesimal_cancel2], simpset()));
 qed "NSLIMSEQ_le";