# HG changeset patch
# User oheimb
# Date 982691608 -3600
# Node ID 8aa53b4591a53bd2adbe1519f6637aa68734e4a1
# Parent  015af2fc7026a660081cccf17c3bcb2a99d244c1
made split_all_tac safe introducing safe_full_simp_tac, EXISTING PROOFS MAY FAIL

diff -r 015af2fc7026 -r 8aa53b4591a5 src/HOL/Algebra/poly/LongDiv.ML
--- a/src/HOL/Algebra/poly/LongDiv.ML	Tue Feb 20 18:48:34 2001 +0100
+++ b/src/HOL/Algebra/poly/LongDiv.ML	Tue Feb 20 18:53:28 2001 +0100
@@ -91,12 +91,10 @@
 by (etac exE 1);
 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);
 by (Clarify_tac 1);
-by (rtac conjI 1);
 by (dtac sym 1);
 by (simp_tac (simpset() addsimps [l_distr, a_assoc]) 1);
 by (Asm_simp_tac 1);
 by (simp_tac (simpset() addsimps a_ac@[smult_l_distr, smult_r_distr, smult_r_minus, smult_assoc2, smult_assoc1]) 1);
-by Auto_tac;
 qed "long_div_eucl_size";
 
 Goal