src/HOL/Polynomial.thy
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