src/HOL/Complex/NSCA.ML
changeset 14374 61de62096768
parent 14373 67a628beb981
child 14377 f454b3004f8f
     1.1 --- a/src/HOL/Complex/NSCA.ML	Tue Feb 03 11:06:36 2004 +0100
     1.2 +++ b/src/HOL/Complex/NSCA.ML	Tue Feb 03 15:58:31 2004 +0100
     1.3 @@ -493,13 +493,13 @@
     1.4  Goal "[| y: CInfinitesimal; x + y = z |] ==> x @c= z";
     1.5  by (rtac (bex_CInfinitesimal_iff RS iffD1) 1);
     1.6  by (dtac (CInfinitesimal_minus_iff RS iffD2) 1);
     1.7 -by (auto_tac (claset(), simpset() addsimps [hcomplex_add_assoc RS sym]));
     1.8 +by (asm_full_simp_tac (simpset() addsimps eq_commute::compare_rls) 1); 
     1.9  qed "CInfinitesimal_add_capprox";
    1.10  
    1.11  Goal "y: CInfinitesimal ==> x @c= x + y";
    1.12  by (rtac (bex_CInfinitesimal_iff RS iffD1) 1);
    1.13  by (dtac (CInfinitesimal_minus_iff RS iffD2) 1);
    1.14 -by (auto_tac (claset(), simpset() addsimps [hcomplex_add_assoc RS sym]));
    1.15 +by (asm_full_simp_tac (simpset() addsimps eq_commute::compare_rls) 1);
    1.16  qed "CInfinitesimal_add_capprox_self";
    1.17  
    1.18  Goal "y: CInfinitesimal ==> x @c= y + x";