src/HOL/Complex/NSCA.ML
changeset 14320 fb7a114826be
parent 14318 7dbd3988b15b
child 14323 27724f528f82
     1.1 --- a/src/HOL/Complex/NSCA.ML	Tue Dec 23 14:45:23 2003 +0100
     1.2 +++ b/src/HOL/Complex/NSCA.ML	Tue Dec 23 14:45:47 2003 +0100
     1.3 @@ -1252,7 +1252,7 @@
     1.4  by (forward_tac [CFinite_minus_iff RS iffD2] 1);
     1.5  by (rtac hcomplex_add_minus_eq_minus 1);
     1.6  by (dtac (stc_add RS sym) 1 THEN assume_tac 1);
     1.7 -by Auto_tac;  
     1.8 +by (asm_simp_tac (simpset() addsimps [add_commute]) 1); 
     1.9  qed "stc_minus";
    1.10  
    1.11  Goalw [hcomplex_diff_def]