src/HOL/Polynomial.thy
 changeset 29475 c06d1b0a970f parent 29474 674a21226c5a child 29478 4a2482e16934
```--- a/src/HOL/Polynomial.thy	Tue Jan 13 08:58:56 2009 -0800
+++ b/src/HOL/Polynomial.thy	Tue Jan 13 10:18:23 2009 -0800
@@ -208,7 +208,7 @@
function
poly_rec :: "'b \<Rightarrow> ('a::zero \<Rightarrow> 'a poly \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a poly \<Rightarrow> 'b"
where
-  poly_rec_pCons_eq_if [simp del]:
+  poly_rec_pCons_eq_if [simp del, code del]:
"poly_rec z f (pCons a p) = f a p (if p = 0 then z else poly_rec z f p)"
by (case_tac x, rename_tac q, case_tac q, auto)

@@ -487,7 +487,7 @@
begin

definition
-  times_poly_def:
+  times_poly_def [code del]:
"p * q = poly_rec 0 (\<lambda>a p pq. smult a q + pCons 0 pq) p"

lemma mult_poly_0_left: "(0::'a poly) * q = 0"
@@ -649,6 +649,7 @@
definition
divmod_poly_rel :: "'a::field poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<Rightarrow> bool"
where
+  [code del]:
"divmod_poly_rel x y q r \<longleftrightarrow>
x = q * y + r \<and> (if y = 0 then q = 0 else r = 0 \<or> degree r < degree y)"
```