summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

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. *}