| changeset 16417 | 9bc16273c2d4 |
| parent 15944 | 9b00875e21f7 |
| child 16639 | 5a89d3622ac0 |
--- a/src/HOL/Algebra/UnivPoly.thy Fri Jun 17 11:35:35 2005 +0200 +++ b/src/HOL/Algebra/UnivPoly.thy Fri Jun 17 16:12:49 2005 +0200 @@ -7,7 +7,7 @@ header {* Univariate Polynomials *} -theory UnivPoly = Module: +theory UnivPoly imports Module begin text {* Polynomials are formalised as modules with additional operations for