doc-src/TutorialI/Trie/document/Option2.tex
changeset 10267 325ead6d9457
parent 9924 3370f6aa3200
equal deleted inserted replaced
10266:41f6be79b44f 10267:325ead6d9457
     1 %
     1 %
     2 \begin{isabellebody}%
     2 \begin{isabellebody}%
     3 \def\isabellecontext{Option2}%
     3 \def\isabellecontext{Option{\isadigit{2}}}%
     4 \isanewline
     4 \isanewline
     5 \isacommand{datatype}\ {\isacharprime}a\ option\ {\isacharequal}\ None\ {\isacharbar}\ Some\ {\isacharprime}a\end{isabellebody}%
     5 \isacommand{datatype}\ {\isacharprime}a\ option\ {\isacharequal}\ None\ {\isacharbar}\ Some\ {\isacharprime}a\end{isabellebody}%
     6 %%% Local Variables:
     6 %%% Local Variables:
     7 %%% mode: latex
     7 %%% mode: latex
     8 %%% TeX-master: "root"
     8 %%% TeX-master: "root"