# 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 ...