--- a/src/HOL/String.thy Thu Nov 08 22:02:07 2018 +0100
+++ b/src/HOL/String.thy Thu Nov 08 22:29:09 2018 +0100
@@ -398,16 +398,16 @@
text \<open>
Logical ground representations for literals are:
- \<^enum> @{text 0} for the empty literal;
+ \<^enum> \<open>0\<close> for the empty literal;
- \<^enum> @{text "Literal b0 \<dots> b6 s"} for a literal starting with one
+ \<^enum> \<open>Literal b0 \<dots> b6 s\<close> for a literal starting with one
character and continued by another literal.
Syntactic representations for literals are:
- \<^enum> Printable text as string prefixed with @{text STR};
+ \<^enum> Printable text as string prefixed with \<open>STR\<close>;
- \<^enum> A single ascii value as numerical hexadecimal value prefixed with @{text STR}.
+ \<^enum> A single ascii value as numerical hexadecimal value prefixed with \<open>STR\<close>.
\<close>
instantiation String.literal :: zero