author | huffman |
Tue, 13 Jan 2009 13:02:16 -0800 | |
changeset 29476 | 68e88293708f |
parent 29475 | c06d1b0a970f |
child 29477 | b834f95c2532 |
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"