src/HOL/Algebra/UnivPoly.thy
changeset 58622 aa99568f56de
parent 57865 dcfb33c26f50
child 60112 3eab4acaa035
--- a/src/HOL/Algebra/UnivPoly.thy	Tue Oct 07 22:54:49 2014 +0200
+++ b/src/HOL/Algebra/UnivPoly.thy	Tue Oct 07 23:12:08 2014 +0200
@@ -18,7 +18,7 @@
   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 the PhD thesis \cite{Ballarin:1999},
+  formalisation of polynomials in the PhD thesis @{cite "Ballarin:1999"},
   which was implemented with axiomatic type classes.  This was later
   ported to Locales.
 *}