--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Misc/document/types.tex	Wed Apr 19 12:59:38 2000 +0200
@@ -0,0 +1,41 @@
+\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}%