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 \<Rightarrow> 'key \<Rightarrow> 'val option";