diff -r 9712294e60b9 -r 15ce4c1c8313 doc-src/Tutorial/Datatype/Trie.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Datatype/Trie.thy	Thu Nov 12 16:45:40 1998 +0100
@@ -0,0 +1,23 @@
+Trie = Main +
+consts   assoc :: "('key * 'val)list => 'key => 'val option"
+primrec "assoc [] x = None"
+        "assoc (p#ps) x =
+           (let (a,b) = p in if a=x then Some b else assoc ps x)"
+datatype ('a,'v)trie = Trie ('v option) "('a * ('a,'v)trie)list"
+consts value :: ('a,'v)trie => 'v option
+       alist :: "('a,'v)trie => ('a * ('a,'v)trie)list"
+primrec "value(Trie ov al) = ov"
+primrec "alist(Trie ov al) = al"
+consts   lookup :: ('a,'v)trie => 'a list => 'v option
+primrec "lookup t [] = value t"
+        "lookup t (a#as) = (case assoc (alist t) a of
+                              None => None
+                            | Some at => lookup at as)"
+consts update :: ('a,'v)trie => 'a list => 'v => ('a,'v)trie
+
+primrec
+  "update t []     v = Trie (Some v) (alist t)"
+  "update t (a#as) v = (let tt = (case assoc (alist t) a of
+                                    None => Trie None [] | Some at => at)
+                        in Trie (value t) ((a,update tt as v)#alist t))"
+end