changeset 9674 | f789d2490669 |
parent 9521 | c396d1092430 |
child 9719 | c753196599f9 |
9673:1b2d4f995b13 | 9674:f789d2490669 |
---|---|
1 \begin{isabelle}% |
1 \begin{isabelle}% |
2 \isanewline |
2 \isanewline |
3 \isacommand{datatype}\ 'a\ option\ =\ None\ |\ Some\ 'a\end{isabelle}% |
3 \isacommand{datatype}\ {\isacharprime}a\ option\ {\isacharequal}\ None\ {\isacharbar}\ Some\ {\isacharprime}a\end{isabelle}% |
4 %%% Local Variables: |
4 %%% Local Variables: |
5 %%% mode: latex |
5 %%% mode: latex |
6 %%% TeX-master: "root" |
6 %%% TeX-master: "root" |
7 %%% End: |
7 %%% End: |