# HG changeset patch # User huffman # Date 1231870703 28800 # Node ID c06d1b0a970f946c896140a6bceac54a74f085c7 # Parent 674a21226c5a285220cab68c8bbe077c5dde2312 declare more definitions [code del] diff -r 674a21226c5a -r c06d1b0a970f src/HOL/Polynomial.thy --- 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 \ ('a::zero \ 'a poly \ 'b \ 'b) \ 'a poly \ '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 (\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 \ 'a poly \ 'a poly \ 'a poly \ bool" where + [code del]: "divmod_poly_rel x y q r \ x = q * y + r \ (if y = 0 then q = 0 else r = 0 \ degree r < degree y)"