--- a/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex Mon Oct 09 09:33:45 2000 +0200
+++ b/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex Mon Oct 09 10:18:21 2000 +0200
@@ -85,7 +85,8 @@
The proof is canonical:%
\end{isamarkuptxt}%
\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ b{\isacharparenright}\isanewline
-\isacommand{by}{\isacharparenleft}auto{\isacharparenright}%
+\isacommand{apply}{\isacharparenleft}auto{\isacharparenright}\isanewline
+\isacommand{done}%
\begin{isamarkuptext}%
\noindent
In fact, all proofs in this case study look exactly like this. Hence we do