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