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