one more [code del] declaration
authorhuffman
Wed, 14 Jan 2009 13:47:14 -0800
changeset 29485 ec072307c69b
parent 29481 3e8420c1124a
child 29486 23a26d17adc0
child 29492 b19b8793b71c
child 29530 9905b660612b
one more [code del] declaration
src/HOL/Fundamental_Theorem_Algebra.thy
--- a/src/HOL/Fundamental_Theorem_Algebra.thy	Wed Jan 14 19:38:55 2009 +0100
+++ b/src/HOL/Fundamental_Theorem_Algebra.thy	Wed Jan 14 13:47:14 2009 -0800
@@ -970,6 +970,7 @@
 definition
   order :: "'a::{idom,recpower} \<Rightarrow> 'a poly \<Rightarrow> nat"
 where
+  [code del]:
   "order a p = (LEAST n. \<not> [:-a, 1:] ^ Suc n dvd p)"
 
 lemma degree_power_le: "degree (p ^ n) \<le> degree p * n"