src/HOL/Algebra/UnivPoly.thy
changeset 14706 71590b7733b7
parent 14666 65f8680c3f16
child 14963 d584e32f7d46
     1.1 --- a/src/HOL/Algebra/UnivPoly.thy	Thu May 06 12:43:00 2004 +0200
     1.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Thu May 06 14:14:18 2004 +0200
     1.3 @@ -1,5 +1,5 @@
     1.4  (*
     1.5 -  Title:     Univariate Polynomials
     1.6 +  Title:     HOL/Algebra/UnivPoly.thy
     1.7    Id:        $Id$
     1.8    Author:    Clemens Ballarin, started 9 December 1996
     1.9    Copyright: Clemens Ballarin
    1.10 @@ -16,10 +16,9 @@
    1.11    carrier set is a set of bounded functions from Nat to the
    1.12    coefficient domain.  Bounded means that these functions return zero
    1.13    above a certain bound (the degree).  There is a chapter on the
    1.14 -  formalisation of polynomials in my PhD thesis
    1.15 -  (\url{http://www4.in.tum.de/~ballarin/publications/}), which was
    1.16 -  implemented with axiomatic type classes.  This was later ported to
    1.17 -  Locales.
    1.18 +  formalisation of polynomials in the PhD thesis \cite{Ballarin:1999},
    1.19 +  which was implemented with axiomatic type classes.  This was later
    1.20 +  ported to Locales.
    1.21  *}
    1.22  
    1.23