--- a/doc-src/TutorialI/Trie/Trie.thy Tue Aug 29 15:43:29 2000 +0200
+++ b/doc-src/TutorialI/Trie/Trie.thy Tue Aug 29 16:05:13 2000 +0200
@@ -109,11 +109,11 @@
txt{*\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: