diff -r 14b2c22a7e40 -r 71590b7733b7 src/HOL/Algebra/UnivPoly.thy
--- 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.
*}