1.1 --- a/src/HOL/Algebra/poly/LongDiv.ML	Tue Feb 20 18:48:34 2001 +0100
     1.2 +++ b/src/HOL/Algebra/poly/LongDiv.ML	Tue Feb 20 18:53:28 2001 +0100
     1.3 @@ -91,12 +91,10 @@
     1.4  by (etac exE 1);
     1.5  by (res_inst_tac [("x", "((%(q,r,k). ((lcoeff g ^ k * lcoeff x) *s monom (deg x - deg g) + q)) xa, (%(q,r,k). r) xa, (%(q,r,k). Suc k) xa)")] exI 1);
     1.6  by (Clarify_tac 1);
     1.7 -by (rtac conjI 1);
     1.8  by (dtac sym 1);
     1.9  by (simp_tac (simpset() addsimps [l_distr, a_assoc]) 1);
    1.10  by (Asm_simp_tac 1);
    1.11  by (simp_tac (simpset() addsimps a_ac@[smult_l_distr, smult_r_distr, smult_r_minus, smult_assoc2, smult_assoc1]) 1);
    1.12 -by Auto_tac;
    1.13  qed "long_div_eucl_size";
    1.14  
    1.15  Goal