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