src/HOL/Complex/CLim.ML

 by (auto_tac (claset(),simpset() addsimps [eq_Abs_hcomplex_ALL,
     starfunC,CInfinitesimal_capprox_minus RS sym,hcomplex_diff,
     CInfinitesimal_hcmod_iff,hcomplex_of_complex_def,
     Infinitesimal_FreeUltrafilterNat_iff,hcmod]));
 by (EVERY1[rtac ccontr, Asm_full_simp_tac]);
-by (fold_tac [real_le_def]);
+by (asm_full_simp_tac (simpset() addsimps [linorder_not_less]) 1);
 by (dtac lemma_skolemize_CLIM2 1);
 by (Step_tac 1);
 by (dres_inst_tac [("x","X")] spec 1);
 by Auto_tac;
 by (dtac (lemma_csimp RS complex_seq_to_hcomplex_CInfinitesimal) 1);

 by (auto_tac (claset(),simpset() addsimps [eq_Abs_hcomplex_ALL,
     starfunCR,hcomplex_diff,hcomplex_of_complex_def,hypreal_diff,
     CInfinitesimal_hcmod_iff,hcmod,Infinitesimal_approx_minus RS sym,
     Infinitesimal_FreeUltrafilterNat_iff]));
 by (EVERY1[rtac ccontr, Asm_full_simp_tac]);
-by (fold_tac [real_le_def]);
+by (asm_full_simp_tac (simpset() addsimps [linorder_not_less]) 1);
 by (dtac lemma_skolemize_CRLIM2 1);
 by (Step_tac 1);
 by (dres_inst_tac [("x","X")] spec 1);
 by Auto_tac;
 by (dtac (lemma_crsimp RS complex_seq_to_hcomplex_CInfinitesimal) 1);