| changeset 17555 | 23c4a349feff |
| parent 16417 | 9bc16273c2d4 |
| child 27015 | f8537d69f514 |
--- a/doc-src/TutorialI/Trie/Trie.thy Wed Sep 21 13:28:44 2005 +0200 +++ b/doc-src/TutorialI/Trie/Trie.thy Wed Sep 21 14:00:28 2005 +0200 @@ -19,7 +19,7 @@ We define two selector functions: *}; -consts value :: "('a,'v)trie \<Rightarrow> 'v option" +consts "value" :: "('a,'v)trie \<Rightarrow> 'v option" alist :: "('a,'v)trie \<Rightarrow> ('a * ('a,'v)trie)list"; primrec "value(Trie ov al) = ov"; primrec "alist(Trie ov al) = al";