diff -r b28bbb153603 -r d666f11ca2d4 doc-src/TutorialI/Trie/Trie.thy --- a/doc-src/TutorialI/Trie/Trie.thy Fri May 18 16:45:55 2001 +0200 +++ b/doc-src/TutorialI/Trie/Trie.thy Fri May 18 17:18:43 2001 +0200 @@ -24,7 +24,8 @@ primrec "alist(Trie ov al) = al"; text{*\noindent -Association lists come with a generic lookup function: +Association lists come with a generic lookup function. Its result +involves type @{text option} because a lookup can fail: *}; consts assoc :: "('key * 'val)list \ 'key \ 'val option";