changeset 15481 | fc075ae929e4 |
parent 15095 | 63f5f4c265dd |
child 15596 | 8665d08085df |
--- a/src/HOL/Algebra/UnivPoly.thy Sun Jan 30 20:48:50 2005 +0100 +++ b/src/HOL/Algebra/UnivPoly.thy Tue Feb 01 18:01:57 2005 +0100 @@ -357,7 +357,7 @@ case 0 then show ?case by (simp add: Pi_def) next case (Suc k) then show ?case - by (subst finsum_Suc2) (simp add: Pi_def a_comm)+ + by (simplesubst finsum_Suc2) (simp add: Pi_def a_comm)+ qed } note l = this