# HG changeset patch
# User ballarin
# Date 1364237624 -3600
# Node ID 237190475d790f2aac1f0108174a3e1f8dbb77e0
# Parent  c3eb0b517ced0f71cecbba53fd04733d944bd8d8
Remove obsolete URLs in documentation of HOL-Algebra.

diff -r c3eb0b517ced -r 237190475d79 src/HOL/Algebra/README.html
--- a/src/HOL/Algebra/README.html	Mon Mar 25 19:53:44 2013 +0100
+++ b/src/HOL/Algebra/README.html	Mon Mar 25 19:53:44 2013 +0100
@@ -51,7 +51,7 @@
 
 <H2>Rings and Polynomials</H2>
 
-<UL><LI>Theory <A HREF="CRing.html"><CODE>CRing</CODE></A>
+<UL><LI>Theory <A HREF="Ring.html"><CODE>CRing</CODE></A>
 defines Abelian monoids and groups.  The difference to commutative
       structures is merely notational:  the binary operation is
       addition rather than multiplication.  Commutative rings are
@@ -108,10 +108,10 @@
 <P>[Jacobson1985] Nathan Jacobson, Basic Algebra I, Freeman, 1985.
 
 <P>[Ballarin1999] Clemens Ballarin, Computer Algebra and Theorem Proving,
-  Author's <A HREF="http://www4.in.tum.de/~ballarin/publications.html">PhD thesis</A>, 1999.
+  Author's PhD thesis, 1999.  Also University of Cambridge, Computer Laboratory Technical Report number 473.
 
 <ADDRESS>
-<P><A HREF="http://www4.in.tum.de/~ballarin">Clemens Ballarin</A>.
+<P><A HREF="http://www21.in.tum.de/~ballarin">Clemens Ballarin</A>.
 </ADDRESS>
 </BODY>
 </HTML>
diff -r c3eb0b517ced -r 237190475d79 src/HOL/Algebra/document/root.bib
--- a/src/HOL/Algebra/document/root.bib	Mon Mar 25 19:53:44 2013 +0100
+++ b/src/HOL/Algebra/document/root.bib	Mon Mar 25 19:53:44 2013 +0100
@@ -4,7 +4,7 @@
   title = 	 {Computer Algebra and Theorem Proving},
   school = 	 {University of Cambridge},
   year = 	 1999,
-  note =	 {\url{http://www4.in.tum.de/~ballarin/publications.html}}
+  note =	 {Also Computer Laboratory Technical Report number 473.}
 }
 
 @Book{Jacobson:1985,