\begin{isabelle}% \isanewline \isacommand{datatype}\ 'a\ option\ =\ None\ |\ Some\ 'a\end{isabelle}% %%% Local Variables: %%% mode: latex %%% TeX-master: "root" %%% End: