changeset 57865 | dcfb33c26f50 |
parent 57512 | cc97b347b301 |
child 58622 | aa99568f56de |
--- a/src/HOL/Algebra/UnivPoly.thy Tue Aug 05 16:21:27 2014 +0200 +++ b/src/HOL/Algebra/UnivPoly.thy Tue Aug 05 16:58:19 2014 +0200 @@ -528,7 +528,7 @@ case 0 with R show ?thesis by simp next case Suc with R show ?thesis - using R.finsum_Suc2 by (simp del: R.finsum_Suc add: R.r_null Pi_def) + using R.finsum_Suc2 by (simp del: R.finsum_Suc add: Pi_def) qed qed (simp_all add: R)