doc-src/TutorialI/Trie/document/Option2.tex
author wenzelm
Sun, 25 Jun 2000 23:48:32 +0200
changeset 9127 b1dc56410b63
parent 8771 026f37a86ea7
child 9145 9f7b8de5bfaf
permissions -rw-r--r--
exception OUTPUT_FAIL of (string * Position.T) * exn (*note: actually belongs to isar_output.ML*);

\begin{isabelle}%
\isanewline
\isacommand{datatype}~'a~option~=~None~|~Some~'a\end{isabelle}%