doc-src/TutorialI/Misc/document/types.tex

cond_add_path;

\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 theories.  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 user-supplied names.
The symbol \indexboldpos{\isasymequiv}{$IsaEq} is a special form of equality
that must 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}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End: