| changeset 13601 | fd3e3d6b37b2 |
| parent 11171 | 8aa53b4591a5 |
| child 13735 | 7de9342aca7a |
--- a/src/HOL/Algebra/poly/LongDiv.ML Mon Sep 30 16:12:16 2002 +0200 +++ b/src/HOL/Algebra/poly/LongDiv.ML Mon Sep 30 16:14:02 2002 +0200 @@ -172,7 +172,7 @@ by (Asm_simp_tac 1); (* proof of 1 *) by (rtac diff_zero_imp_eq 1); -by (Asm_full_simp_tac 1); +by (hyp_subst_tac 1); by (dres_inst_tac [("a", "?x+?y")] eq_imp_diff_zero 1); by (asm_full_simp_tac (simpset() addsimps (l_distr::minus_add::l_minus::a_ac)) 1); qed "long_div_quo_unique";