Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
merged
authorwenzelm
Thu, 15 Jan 2009 00:44:19 +0100
changeset 29486 23a26d17adc0
parent 29485 ec072307c69b (diff)
parent 29484 15863d782ae3 (current diff)
child 29487 06f4bb9fdb85
merged
--- 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"
isabelle