summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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