--- a/doc-src/TutorialI/Trie/document/Trie.tex Tue Aug 29 15:43:29 2000 +0200
+++ b/doc-src/TutorialI/Trie/document/Trie.tex Tue Aug 29 16:05:13 2000 +0200
@@ -98,11 +98,11 @@
\begin{isamarkuptxt}%
\noindent
Unfortunately, this time we are left with three intimidating looking subgoals:
-\begin{isabellepar}%
+\begin{isabelle}
~1.~\dots~{\isasymLongrightarrow}~lookup~\dots~bs~=~lookup~t~bs\isanewline
~2.~\dots~{\isasymLongrightarrow}~lookup~\dots~bs~=~lookup~t~bs\isanewline
~3.~\dots~{\isasymLongrightarrow}~lookup~\dots~bs~=~lookup~t~bs%
-\end{isabellepar}%
+\end{isabelle}
Clearly, if we want to make headway we have to instantiate \isa{bs} as
well now. It turns out that instead of induction, case distinction
suffices:%