| changeset 63680 | 6e1e8b5abbfa |
| parent 62910 | f37878ebba65 |
| child 69597 | ff784d5a5bfb |
--- a/src/HOL/ex/ML.thy Fri Aug 12 17:49:02 2016 +0200 +++ b/src/HOL/ex/ML.thy Fri Aug 12 17:53:55 2016 +0200 @@ -94,7 +94,7 @@ ML \<open>factorial 42\<close> ML \<open>factorial 10000 div factorial 9999\<close> -text \<open>See @{url "http://mathworld.wolfram.com/AckermannFunction.html"}\<close> +text \<open>See \<^url>\<open>http://mathworld.wolfram.com/AckermannFunction.html\<close>.\<close> ML \<open> fun ackermann 0 n = n + 1