diff -r 966974a7a5b3 -r c613cd06d5cf doc-src/TutorialI/Trie/document/Trie.tex --- 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}