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