Added brief intro text.
authorballarin
Tue Apr 13 13:53:54 2004 +0200 (2004-04-13)
changeset 145534740fc2da7bb
parent 14552 e88f52b775a5
child 14554 b9cd48af3512
Added brief intro text.
src/HOL/Algebra/UnivPoly.thy
     1.1 --- a/src/HOL/Algebra/UnivPoly.thy	Tue Apr 13 10:45:35 2004 +0200
     1.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Tue Apr 13 13:53:54 2004 +0200
     1.3 @@ -9,6 +9,19 @@
     1.4  
     1.5  section {* Univariate Polynomials *}
     1.6  
     1.7 +text {*
     1.8 +  Polynomials are formalised as modules with additional operations for 
     1.9 +  extracting coefficients from polynomials and for obtaining monomials 
    1.10 +  from coefficients and exponents (record @{text "up_ring"}).
    1.11 +  The carrier set is 
    1.12 +  a set of bounded functions from Nat to the coefficient domain.  
    1.13 +  Bounded means that these functions return zero above a certain bound 
    1.14 +  (the degree).  There is a chapter on the formalisation of polynomials 
    1.15 +  in my PhD thesis (http://www4.in.tum.de/\~{}ballarin/publications/), 
    1.16 +  which was implemented with axiomatic type classes.  This was later
    1.17 +  ported to Locales.
    1.18 +*}
    1.19 +
    1.20  subsection {* The Constructor for Univariate Polynomials *}
    1.21  
    1.22  (* Could alternatively use locale ...