--- a/src/HOL/Algebra/poly/LongDiv.thy Sun Jan 30 20:48:50 2005 +0100
+++ b/src/HOL/Algebra/poly/LongDiv.thy Tue Feb 01 18:01:57 2005 +0100
@@ -18,12 +18,10 @@
"!! f::(nat=>'a::ring). (ALL i. i < m --> f i = 0) -->
setsum (%i. f (i+m)) {..d} = setsum f {..m+d}"
apply (induct_tac d)
- apply (induct_tac m)
- apply (simp)
- apply (force)
- apply (simp)
- apply (subst ab_semigroup_add.add_commute[of m])
- apply (simp)
+ apply (induct_tac m)
+ apply (simp)
+ apply (force)
+ apply (simp add: ab_semigroup_add.add_commute[of m])
done
end