doc-src/TutorialI/Trie/document/Option2.tex
author paulson
Thu, 01 Jun 2000 13:28:00 +0200
changeset 9014 4382883421ec
parent 8771 026f37a86ea7
child 9145 9f7b8de5bfaf
permissions -rw-r--r--
simplified the proof of nth_upt

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