# HG changeset patch
# User wenzelm
# Date 1231976659 -3600
# Node ID 23a26d17adc01256aa6b8c830a98000c446fe549
# Parent  ec072307c69bd8e527bb09a981384f37eaa18127# Parent  15863d782ae39099b984fa283b46e18cfcf672bb
merged

diff -r 15863d782ae3 -r 23a26d17adc0 src/HOL/Fundamental_Theorem_Algebra.thy
--- a/src/HOL/Fundamental_Theorem_Algebra.thy	Thu Jan 15 00:44:06 2009 +0100
+++ b/src/HOL/Fundamental_Theorem_Algebra.thy	Thu Jan 15 00:44:19 2009 +0100
@@ -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"