| changeset 63680 | 6e1e8b5abbfa |
| parent 62348 | 9a5f43dac883 |
| child 64974 | d0e55f85fd8a |
--- a/src/HOL/ex/NatSum.thy Fri Aug 12 17:49:02 2016 +0200 +++ b/src/HOL/ex/NatSum.thy Fri Aug 12 17:53:55 2016 +0200 @@ -10,7 +10,7 @@ Summing natural numbers, squares, cubes, etc. Thanks to Sloane's On-Line Encyclopedia of Integer Sequences, - @{url "http://www.research.att.com/~njas/sequences/"}. + \<^url>\<open>http://www.research.att.com/~njas/sequences\<close>. \<close> lemmas [simp] =