--- 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