changeset 29476 | 68e88293708f |
parent 29472 | a63a2e46cec9 |
child 29478 | 4a2482e16934 |
--- a/src/HOL/Fundamental_Theorem_Algebra.thy Tue Jan 13 10:18:23 2009 -0800 +++ b/src/HOL/Fundamental_Theorem_Algebra.thy Tue Jan 13 13:02:16 2009 -0800 @@ -134,7 +134,7 @@ apply (simp add: offset_poly_eq_0_iff) done -definition +definition [code del]: "plength p = (if p = 0 then 0 else Suc (degree p))" lemma plength_eq_0_iff [simp]: "plength p = 0 \<longleftrightarrow> p = 0"