src/HOL/ex/Sudoku.thy

--- a/src/HOL/ex/Sudoku.thy	Fri Aug 12 17:49:02 2016 +0200
+++ b/src/HOL/ex/Sudoku.thy	Fri Aug 12 17:53:55 2016 +0200
@@ -136,7 +136,7 @@
 
 text \<open>
   Some ``exceptionally difficult'' Sudokus, taken from
-  @{url "http://en.wikipedia.org/w/index.php?title=Algorithmics_of_sudoku&oldid=254685903"}
+  \<^url>\<open>http://en.wikipedia.org/w/index.php?title=Algorithmics_of_sudoku&oldid=254685903\<close>
   (accessed December~2, 2008).
 \<close>