src/HOL/Polynomial.thy
2009-01-15 huffman 2009-01-15 rename divmod_poly to pdivmod
2009-01-13 huffman 2009-01-13 declare pCons_0_0 [code post]
2009-01-13 huffman 2009-01-13 code generation for polynomials
2009-01-13 huffman 2009-01-13 declare more definitions [code del]
2009-01-13 huffman 2009-01-13 define polynomial multiplication using poly_rec
2009-01-13 huffman 2009-01-13 declare smult rules [simp]
2009-01-13 huffman 2009-01-13 simplify proof of coeff_mult_degree_sum
2009-01-12 huffman 2009-01-12 add lemmas poly_power, poly_roots_finite
2009-01-12 huffman 2009-01-12 new lemmas about synthetic_div; declare degree_pCons_eq_if [simp]
2009-01-12 huffman 2009-01-12 correctness and uniqueness of synthetic division
2009-01-12 huffman 2009-01-12 add synthetic division algorithm for polynomials
2009-01-12 huffman 2009-01-12 add list-style syntax for pCons
2009-01-12 huffman 2009-01-12 add recursion combinator poly_rec; define poly function using poly_rec
2009-01-12 huffman 2009-01-12 add lemmas degree_{add,diff}_less
2009-01-11 huffman 2009-01-11 new theory of polynomials