src/Doc/Tutorial/Misc/types.thy

 
 subsection\<open>Constant Definitions\<close>
 
 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>
 
 definition nand :: gate where "nand A B \<equiv> \<not>(A \<and> B)"
 definition xor  :: gate where "xor  A B \<equiv> A \<and> \<not>B \<or> \<not>A \<and> B"

 The symbol \indexboldpos{\isasymequiv}{$IsaEq} is a special form of equality
 that must be used in constant definitions.
 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(*>*)