\begin{isabelle}%
\isacommand{types}~number~~~~~~~=~nat\isanewline
~~~~~~gate~~~~~~~~~=~{"}bool~{\isasymRightarrow}~bool~{\isasymRightarrow}~bool{"}\isanewline
~~~~~~('a,'b)alist~=~{"}('a~*~'b)list{"}%
\begin{isamarkuptext}%
\noindent\indexbold{*types}%
Internally all synonyms are fully expanded. As a consequence Isabelle's
output never contains synonyms. Their main purpose is to improve the
readability of theory definitions. Synonyms can be used just like any other
type:%
\end{isamarkuptext}%
\isacommand{consts}~nand~::~gate\isanewline
~~~~~~~exor~::~gate%
\begin{isamarkuptext}%
\subsection{Constant definitions}
\label{sec:ConstDefinitions}
\indexbold{definition}
The above constants \isa{nand} and \isa{exor} are non-recursive and can
therefore be defined directly by%
\end{isamarkuptext}%
\isacommand{defs}~nand\_def:~{"}nand~A~B~{\isasymequiv}~{\isasymnot}(A~{\isasymand}~B){"}\isanewline
~~~~~exor\_def:~{"}exor~A~B~{\isasymequiv}~A~{\isasymand}~{\isasymnot}B~{\isasymor}~{\isasymnot}A~{\isasymand}~B{"}%
\begin{isamarkuptext}%
\noindent%
where \isacommand{defs}\indexbold{*defs} is a keyword and \isa{nand_def} and
\isa{exor_def} are arbitrary user-supplied names.
The symbol \indexboldpos{\isasymequiv}{$IsaEq} is a special form of equality
that should only be used in constant definitions.
Declarations and definitions can also be merged%
\end{isamarkuptext}%
\isacommand{constdefs}~nor~::~gate\isanewline
~~~~~~~~~{"}nor~A~B~{\isasymequiv}~{\isasymnot}(A~{\isasymor}~B){"}\isanewline
~~~~~~~~~~exor2~::~gate\isanewline
~~~~~~~~~{"}exor2~A~B~{\isasymequiv}~(A~{\isasymor}~B)~{\isasymand}~({\isasymnot}A~{\isasymor}~{\isasymnot}B){"}%
\begin{isamarkuptext}%
\noindent\indexbold{*constdefs}%
in which case the default name of each definition is \isa{$f$_def}, where
$f$ is the name of the defined constant.%
\end{isamarkuptext}%
\end{isabelle}%