diff -r 3daeba5130f0 -r 499f92dc6e45 src/HOL/Library/Kleene_Algebra.thy
--- a/src/HOL/Library/Kleene_Algebra.thy	Mon Dec 09 12:16:52 2013 +0100
+++ b/src/HOL/Library/Kleene_Algebra.thy	Mon Dec 09 12:22:23 2013 +0100
@@ -14,7 +14,7 @@
 text {* Various lemmas correspond to entries in a database of theorems
   about Kleene algebras and related structures maintained by Peter
   H\"ofner: see
-  \url{http://www.informatik.uni-augsburg.de/~hoefnepe/kleene_db/lemmas/index.html}. *}
+  @{url "http://www.informatik.uni-augsburg.de/~hoefnepe/kleene_db/lemmas/index.html"}. *}
 
 subsection {* Preliminaries *}