author | ballarin |

Tue Apr 13 13:53:54 2004 +0200 (2004-04-13) | |

changeset 14553 | 4740fc2da7bb |

parent 14552 | e88f52b775a5 |

child 14554 | b9cd48af3512 |

Added brief intro text.

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