summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Algebra/UnivPoly.thy

changeset 26934 | c1ae80a58341 |

parent 26202 | 51f8a696cd8d |

child 27611 | 2c01c0bdb385 |

1.1 --- a/src/HOL/Algebra/UnivPoly.thy Sat May 17 21:46:24 2008 +0200 1.2 +++ b/src/HOL/Algebra/UnivPoly.thy Sat May 17 23:37:07 2008 +0200 1.3 @@ -483,6 +483,7 @@ 1.4 proof (cases "k = Suc n") 1.5 case True show ?thesis 1.6 proof - 1.7 + fix m 1.8 from True have less_add_diff: 1.9 "!!i. [| n < i; i <= n + m |] ==> n + m - i < m" by arith 1.10 from True have "coeff P (monom P \<one> (Suc n)) k = \<one>" by simp