diff -r 5b6305cab436 -r 9feb1e0c4cb3 doc-src/TutorialI/Trie/document/Trie.tex
--- a/doc-src/TutorialI/Trie/document/Trie.tex	Tue Sep 12 14:59:44 2000 +0200
+++ b/doc-src/TutorialI/Trie/document/Trie.tex	Tue Sep 12 15:43:15 2000 +0200
@@ -72,8 +72,7 @@
 expand all \isa{let}s and to split all \isa{case}-constructs over
 options:%
 \end{isamarkuptext}%
-\isacommand{lemmas}\ {\isacharbrackleft}simp{\isacharbrackright}\ {\isacharequal}\ Let{\isacharunderscore}def\isanewline
-\isacommand{lemmas}\ {\isacharbrackleft}split{\isacharbrackright}\ {\isacharequal}\ option{\isachardot}split%
+\isacommand{declare}\ Let{\isacharunderscore}def{\isacharbrackleft}simp{\isacharbrackright}\ option{\isachardot}split{\isacharbrackleft}split{\isacharbrackright}%
 \begin{isamarkuptext}%
 \noindent
 The reason becomes clear when looking (probably after a failed proof