doc-src/TutorialI/Trie/Trie.thy

--- a/doc-src/TutorialI/Trie/Trie.thy	Tue Sep 12 14:59:44 2000 +0200
+++ b/doc-src/TutorialI/Trie/Trie.thy	Tue Sep 12 15:43:15 2000 +0200
@@ -81,8 +81,7 @@
 options:
 *};
 
-lemmas [simp] = Let_def;
-lemmas [split] = option.split;
+declare Let_def[simp] option.split[split]
 
 text{*\noindent
 The reason becomes clear when looking (probably after a failed proof