--- a/src/HOL/Nominal/Examples/CK_Machine.thy Mon Dec 09 12:16:52 2013 +0100
+++ b/src/HOL/Nominal/Examples/CK_Machine.thy Mon Dec 09 12:22:23 2013 +0100
@@ -16,8 +16,8 @@
by Roshan James (Indiana University) and also by the lecture notes
written by Andy Pitts for his semantics course. See
- http://www.cs.indiana.edu/~rpjames/lm.pdf
- http://www.cl.cam.ac.uk/teaching/2001/Semantics/
+ @{url "http://www.cs.indiana.edu/~rpjames/lm.pdf"}
+ @{url "http://www.cl.cam.ac.uk/teaching/2001/Semantics/"}
*}