# HG changeset patch # User ballarin # Date 1081857234 -7200 # Node ID 4740fc2da7bbb49a1dfb1e5dd974096066f68736 # Parent e88f52b775a5c93351bfa3065dee635d11ef9154 Added brief intro text. diff -r e88f52b775a5 -r 4740fc2da7bb src/HOL/Algebra/UnivPoly.thy --- a/src/HOL/Algebra/UnivPoly.thy Tue Apr 13 10:45:35 2004 +0200 +++ b/src/HOL/Algebra/UnivPoly.thy Tue Apr 13 13:53:54 2004 +0200 @@ -9,6 +9,19 @@ section {* Univariate Polynomials *} +text {* + Polynomials are formalised as modules with additional operations for + extracting coefficients from polynomials and for obtaining monomials + from coefficients and exponents (record @{text "up_ring"}). + The carrier set is + a set of bounded functions from Nat to the coefficient domain. + Bounded means that these functions return zero above a certain bound + (the degree). There is a chapter on the formalisation of polynomials + in my PhD thesis (http://www4.in.tum.de/\~{}ballarin/publications/), + which was implemented with axiomatic type classes. This was later + ported to Locales. +*} + subsection {* The Constructor for Univariate Polynomials *} (* Could alternatively use locale ...