diff -r ff6787d730d5 -r 260090b54ef9 doc-src/Exercises/2001/a3/Trie3.thy
--- a/doc-src/Exercises/2001/a3/Trie3.thy	Fri Apr 29 18:13:28 2005 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,19 +0,0 @@
-(*<*)
-theory Trie3 = Main:
-(*>*)
-
-text {* Instead of association lists we can also use partial functions
-that map letters to subtrees. Partiality can be modelled with the help
-of type @{typ "'a option"}: if @{term f} is a function of type
-\mbox{@{typ "'a \<Rightarrow> 'b option"}}, set @{term "f a = Some b"}
-if @{term a} should be mapped to some @{term b} and set @{term "f a =
-None"} otherwise.  *}
-
-datatype ('a, 'v) trie = Trie  "'v option" "'a \<Rightarrow> ('a,'v) trie option";
-
-text{* Modify the definitions of @{term lookup} and @{term modify}
-accordingly and show the same correctness theorem as above. *}
-
-(*<*)
-end;
-(*>*)