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