# HG changeset patch
# User paulson
# Date 980160329 -3600
# Node ID 64c26f32674312f1d626e284771a8bf55f39d0b0
# Parent  fd582f0d649b2825cf52e794756f337b8e60cfe1
tided

diff -r fd582f0d649b -r 64c26f326743 src/HOL/Algebra/poly/LongDiv.ML
--- a/src/HOL/Algebra/poly/LongDiv.ML	Mon Jan 22 11:02:53 2001 +0100
+++ b/src/HOL/Algebra/poly/LongDiv.ML	Mon Jan 22 11:45:29 2001 +0100
@@ -17,12 +17,10 @@
 by (Clarify_tac 1);
 by (Asm_full_simp_tac 1);
 (* case "deg q ~= m" *)
-by (dtac le_neq_implies_less 1 THEN atac 1);
-by (dres_inst_tac [("i", "deg p")] le_less_trans 1); by (assume_tac 1);
-by (dres_inst_tac [("i", "deg q")] le_less_trans 1); by (assume_tac 1);
+by (arith_tac 2);
+by (subgoal_tac "deg p < m & deg q < m" 1);
 by (asm_simp_tac (simpset() addsimps [deg_aboveD]) 1);
-(* end case *)
-by (asm_full_simp_tac (simpset() addsimps [le_pred_eq]) 1);
+by (arith_tac 1);
 qed "deg_lcoeff_cancel";
 
 Goal