--- a/src/HOL/Library/Univ_Poly.thy Wed Oct 12 16:21:07 2011 +0200
+++ b/src/HOL/Library/Univ_Poly.thy Wed Oct 12 20:16:48 2011 +0200
@@ -118,13 +118,13 @@
qed
lemma (in comm_semiring_0) padd_assoc: "\<forall>b c. (a +++ b) +++ c = a +++ (b +++ c)"
-apply (induct a arbitrary: b c)
+apply (induct a)
apply (simp, clarify)
apply (case_tac b, simp_all add: add_ac)
done
lemma (in semiring_0) poly_cmult_distr: "a %* ( p +++ q) = (a %* p +++ a %* q)"
-apply (induct p arbitrary: q,simp)
+apply (induct p arbitrary: q, simp)
apply (case_tac q, simp_all add: right_distrib)
done