--- a/doc-src/TutorialI/Misc/document/types.tex Tue Aug 16 13:42:21 2005 +0200
+++ b/doc-src/TutorialI/Misc/document/types.tex Tue Aug 16 13:42:23 2005 +0200
@@ -1,10 +1,23 @@
%
\begin{isabellebody}%
\def\isabellecontext{types}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
\isamarkupfalse%
\isacommand{types}\ number\ \ \ \ \ \ \ {\isacharequal}\ nat\isanewline
\ \ \ \ \ \ gate\ \ \ \ \ \ \ \ \ {\isacharequal}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\isanewline
-\ \ \ \ \ \ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}alist\ {\isacharequal}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}list{\isachardoublequote}\isamarkupfalse%
+\ \ \ \ \ \ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}alist\ {\isacharequal}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}list{\isachardoublequote}\isamarkuptrue%
%
\begin{isamarkuptext}%
\noindent
@@ -13,9 +26,9 @@
readability of theories. Synonyms can be used just like any other
type. Here, we declare two constants of type \isa{gate}:%
\end{isamarkuptext}%
-\isamarkuptrue%
+\isamarkupfalse%
\isacommand{consts}\ nand\ {\isacharcolon}{\isacharcolon}\ gate\isanewline
-\ \ \ \ \ \ \ xor\ \ {\isacharcolon}{\isacharcolon}\ gate\isamarkupfalse%
+\ \ \ \ \ \ \ xor\ \ {\isacharcolon}{\isacharcolon}\ gate\isamarkuptrue%
%
\isamarkupsubsection{Constant Definitions%
}
@@ -26,9 +39,9 @@
The constants \isa{nand} and \isa{xor} above are non-recursive and can
be defined directly:%
\end{isamarkuptext}%
-\isamarkuptrue%
+\isamarkupfalse%
\isacommand{defs}\ nand{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}nand\ A\ B\ {\isasymequiv}\ {\isasymnot}{\isacharparenleft}A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequote}\isanewline
-\ \ \ \ \ xor{\isacharunderscore}def{\isacharcolon}\ \ {\isachardoublequote}xor\ A\ B\ \ {\isasymequiv}\ A\ {\isasymand}\ {\isasymnot}B\ {\isasymor}\ {\isasymnot}A\ {\isasymand}\ B{\isachardoublequote}\isamarkupfalse%
+\ \ \ \ \ xor{\isacharunderscore}def{\isacharcolon}\ \ {\isachardoublequote}xor\ A\ B\ \ {\isasymequiv}\ A\ {\isasymand}\ {\isasymnot}B\ {\isasymor}\ {\isasymnot}A\ {\isasymand}\ B{\isachardoublequote}\isamarkuptrue%
%
\begin{isamarkuptext}%
\noindent%
@@ -45,19 +58,30 @@
\isacommand{defs}. For instance, we can introduce \isa{nand} and \isa{xor} by a
single command:%
\end{isamarkuptext}%
-\isamarkuptrue%
+\isamarkupfalse%
\isacommand{constdefs}\ nor\ {\isacharcolon}{\isacharcolon}\ gate\isanewline
\ \ \ \ \ \ \ \ \ {\isachardoublequote}nor\ A\ B\ {\isasymequiv}\ {\isasymnot}{\isacharparenleft}A\ {\isasymor}\ B{\isacharparenright}{\isachardoublequote}\isanewline
\ \ \ \ \ \ \ \ \ \ xor{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ gate\isanewline
-\ \ \ \ \ \ \ \ \ {\isachardoublequote}xor{\isadigit{2}}\ A\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymor}\ B{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}{\isasymnot}A\ {\isasymor}\ {\isasymnot}B{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
+\ \ \ \ \ \ \ \ \ {\isachardoublequote}xor{\isadigit{2}}\ A\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymor}\ B{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}{\isasymnot}A\ {\isasymor}\ {\isasymnot}B{\isacharparenright}{\isachardoublequote}\isamarkuptrue%
%
\begin{isamarkuptext}%
\noindent
The default name of each definition is $f$\isa{{\isacharunderscore}def}, where
$f$ is the name of the defined constant.%
\end{isamarkuptext}%
-\isamarkuptrue%
-\isamarkupfalse%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex