| changeset 14577 | dbb95b825244 |
| parent 14553 | 4740fc2da7bb |
| child 14590 | 276ef51cedbf |
--- a/src/HOL/Algebra/UnivPoly.thy Fri Apr 16 04:06:52 2004 +0200 +++ b/src/HOL/Algebra/UnivPoly.thy Fri Apr 16 04:07:10 2004 +0200 @@ -5,9 +5,9 @@ Copyright: Clemens Ballarin *) -theory UnivPoly = Module: +header {* Univariate Polynomials *} -section {* Univariate Polynomials *} +theory UnivPoly = Module: text {* Polynomials are formalised as modules with additional operations for