--- a/doc-src/TutorialI/Trie/document/Trie.tex Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/Trie/document/Trie.tex Fri Jul 28 16:02:51 2000 +0200
@@ -44,7 +44,7 @@
distinguishes the two cases whether the search string is empty or not:%
\end{isamarkuptext}%
\isacommand{lemma}~[simp]:~{"}lookup~(Trie~None~[])~as~=~None{"}\isanewline
-\isacommand{apply}(case\_tac~as,~auto)\isacommand{.}%
+\isacommand{by}(case\_tac~as,~auto)%
\begin{isamarkuptext}%
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
@@ -107,7 +107,7 @@
suffices:%
\end{isamarkuptxt}%
\isacommand{apply}(case\_tac[!]~bs)\isanewline
-\isacommand{apply}(auto)\isacommand{.}%
+\isacommand{by}(auto)%
\begin{isamarkuptext}%
\noindent
Both \isaindex{case_tac} and \isaindex{induct_tac}