--- a/src/Doc/Tutorial/Misc/types.thy Wed Dec 26 16:07:28 2018 +0100
+++ b/src/Doc/Tutorial/Misc/types.thy Wed Dec 26 16:25:20 2018 +0100
@@ -14,7 +14,7 @@
text\<open>\label{sec:ConstDefinitions}\indexbold{definitions}%
Nonrecursive definitions can be made with the \commdx{definition}
-command, for example @{text nand} and @{text xor} gates
+command, for example \<open>nand\<close> and \<open>xor\<close> gates
(based on type @{typ gate} above):
\<close>
@@ -27,6 +27,6 @@
Pattern-matching is not allowed: each definition must be of
the form $f\,x@1\,\dots\,x@n~\isasymequiv~t$.
Section~\ref{sec:Simp-with-Defs} explains how definitions are used
-in proofs. The default name of each definition is $f$@{text"_def"}, where
+in proofs. The default name of each definition is $f$\<open>_def\<close>, where
$f$ is the name of the defined constant.\<close>
(*<*)end(*>*)