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

 %
 \begin{isabellebody}%
 \def\isabellecontext{types}%
+\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}%
+\ \ \ \ \ \ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}alist\ {\isacharequal}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}list{\isachardoublequote}\isamarkupfalse%
+%
 \begin{isamarkuptext}%
 \noindent
 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.  Here, we declare two constants of type \isa{gate}:%
 \end{isamarkuptext}%
+\isamarkuptrue%
 \isacommand{consts}\ nand\ {\isacharcolon}{\isacharcolon}\ gate\isanewline
-\ \ \ \ \ \ \ xor\ \ {\isacharcolon}{\isacharcolon}\ gate%
+\ \ \ \ \ \ \ xor\ \ {\isacharcolon}{\isacharcolon}\ gate\isamarkupfalse%
+%
 \isamarkupsubsection{Constant Definitions%
 }
+\isamarkuptrue%
 %
 \begin{isamarkuptext}%
 \label{sec:ConstDefinitions}\indexbold{definitions}%
 The constants \isa{nand} and \isa{xor} above are non-recursive and can 
 be defined directly:%
 \end{isamarkuptext}%
+\isamarkuptrue%
 \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}%
+\ \ \ \ \ xor{\isacharunderscore}def{\isacharcolon}\ \ {\isachardoublequote}xor\ A\ B\ \ {\isasymequiv}\ A\ {\isasymand}\ {\isasymnot}B\ {\isasymor}\ {\isasymnot}A\ {\isasymand}\ B{\isachardoublequote}\isamarkupfalse%
+%
 \begin{isamarkuptext}%
 \noindent%
 Here \commdx{defs} is a keyword and
 \isa{nand{\isacharunderscore}def} and \isa{xor{\isacharunderscore}def} are user-supplied names.
 The symbol \indexboldpos{\isasymequiv}{$IsaEq} is a special form of equality

 
 A \commdx{constdefs} command combines the effects of \isacommand{consts} and 
 \isacommand{defs}.  For instance, we can introduce \isa{nand} and \isa{xor} by a 
 single command:%
 \end{isamarkuptext}%
+\isamarkuptrue%
 \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}%
+\ \ \ \ \ \ \ \ \ {\isachardoublequote}xor{\isadigit{2}}\ A\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymor}\ B{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}{\isasymnot}A\ {\isasymor}\ {\isasymnot}B{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
+%
 \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%
 \end{isabellebody}%
 %%% Local Variables:
 %%% mode: latex
 %%% TeX-master: "root"
 %%% End: