--- a/doc-src/TutorialI/Trie/document/Trie.tex Wed Oct 11 09:09:06 2000 +0200
+++ b/doc-src/TutorialI/Trie/document/Trie.tex Wed Oct 11 10:44:42 2000 +0200
@@ -114,8 +114,8 @@
\noindent
All methods ending in \isa{tac} take an optional first argument that
specifies the range of subgoals they are applied to, where \isa{{\isacharbrackleft}{\isacharbang}{\isacharbrackright}} means
-all subgoals, i.e.\ \isa{{\isacharbrackleft}\isadigit{1}{\isacharminus}\isadigit{3}{\isacharbrackright}} in our case. Individual subgoal numbers,
-e.g. \isa{{\isacharbrackleft}\isadigit{2}{\isacharbrackright}} are also allowed.
+all subgoals, i.e.\ \isa{{\isacharbrackleft}{\isadigit{1}}{\isacharminus}{\isadigit{3}}{\isacharbrackright}} in our case. Individual subgoal numbers,
+e.g. \isa{{\isacharbrackleft}{\isadigit{2}}{\isacharbrackright}} are also allowed.
This proof may look surprisingly straightforward. However, note that this
comes at a cost: the proof script is unreadable because the intermediate