--- a/src/HOL/String.thy Fri Jan 04 21:49:06 2019 +0100
+++ b/src/HOL/String.thy Fri Jan 04 23:22:53 2019 +0100
@@ -10,7 +10,7 @@
text \<open>
When modelling strings, we follow the approach given
- in @{url "https://utf8everywhere.org/"}:
+ in \<^url>\<open>https://utf8everywhere.org/\<close>:
\<^item> Strings are a list of bytes (8 bit).
@@ -668,9 +668,9 @@
| constant "(\<le>) :: String.literal \<Rightarrow> String.literal \<Rightarrow> bool" \<rightharpoonup>
(SML) "!((_ : string) <= _)"
and (OCaml) "!((_ : string) <= _)"
- \<comment> \<open>Order operations for @{typ String.literal} work in Haskell only
+ \<comment> \<open>Order operations for \<^typ>\<open>String.literal\<close> work in Haskell only
if no type class instance needs to be generated, because String = [Char] in Haskell
- and @{typ "char list"} need not have the same order as @{typ String.literal}.\<close>
+ and \<^typ>\<open>char list\<close> need not have the same order as \<^typ>\<open>String.literal\<close>.\<close>
and (Haskell) infix 4 "<="
and (Scala) infixl 4 "<="
and (Eval) infixl 6 "<="