diff -r 02c51ca9c531 -r d17c0b34d5c8 doc-src/TutorialI/Trie/document/Trie.tex
--- a/doc-src/TutorialI/Trie/document/Trie.tex	Fri Aug 04 23:02:11 2000 +0200
+++ b/doc-src/TutorialI/Trie/document/Trie.tex	Sun Aug 06 15:26:53 2000 +0200
@@ -70,8 +70,8 @@
 expand all \isa{let}s and to split all \isa{case}-constructs over
 options:%
 \end{isamarkuptext}%
-\isacommand{theorems}\ [simp]\ =\ Let\_def\isanewline
-\isacommand{theorems}\ [split]\ =\ option.split%
+\isacommand{lemmas}\ [simp]\ =\ Let\_def\isanewline
+\isacommand{lemmas}\ [split]\ =\ option.split%
 \begin{isamarkuptext}%
 \noindent
 The reason becomes clear when looking (probably after a failed proof
@@ -106,14 +106,13 @@
 well now. It turns out that instead of induction, case distinction
 suffices:%
 \end{isamarkuptxt}%
-\isacommand{apply}(case\_tac[!]\ bs)\isanewline
-\isacommand{by}(auto)%
+\isacommand{by}(case\_tac[!]\ bs,\ auto)%
 \begin{isamarkuptext}%
 \noindent
-Both \isaindex{case_tac} and \isaindex{induct_tac}
-take an optional first argument that specifies the range of subgoals they are
-applied to, where \isa{!} means all subgoals, i.e.\ \isa{[1-3]} in our case. Individual
-subgoal numbers are also allowed.
+All methods ending in \isa{tac} take an optional first argument that
+specifies the range of subgoals they are applied to, where \isa{[!]} means all
+subgoals, i.e.\ \isa{[1-3]} in our case. Individual subgoal numbers,
+e.g. \isa{[2]} are also allowed.
 
 This proof may look surprisingly straightforward. However, note that this
 comes at a cost: the proof script is unreadable because the