
diff -r 5a4d78204492 -r 7c4ec77a8715 doc-src/TutorialI/Trie/Trie.thy
--- a/doc-src/TutorialI/Trie/Trie.thy	Thu Nov 29 13:33:45 2001 +0100
+++ b/doc-src/TutorialI/Trie/Trie.thy	Thu Nov 29 14:12:42 2001 +0100
@@ -59,7 +59,7 @@
 
 text{*
 Things begin to get interesting with the definition of an update function
-that adds a new (string,value) pair to a trie, overwriting the old value
+that adds a new (string, value) pair to a trie, overwriting the old value
 associated with that string:
 *};
 




