diff -r 966974a7a5b3 -r c613cd06d5cf doc-src/TutorialI/Ifexpr/document/Ifexpr.tex
--- a/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex	Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex	Fri Jul 28 16:02:51 2000 +0200
@@ -74,7 +74,7 @@
 The proof is canonical:%
 \end{isamarkuptxt}%
 \isacommand{apply}(induct\_tac~b)\isanewline
-\isacommand{apply}(auto)\isacommand{.}%
+\isacommand{by}(auto)%
 \begin{isamarkuptext}%
 \noindent
 In fact, all proofs in this case study look exactly like this. Hence we do
@@ -131,7 +131,7 @@
 and prove \isa{normal(norm b)}. Of course, this requires a lemma about
 normality of \isa{normif}:%
 \end{isamarkuptext}%
-\isacommand{lemma}~[simp]:~{"}{\isasymforall}t~e.~normal(normif~b~t~e)~=~(normal~t~{\isasymand}~normal~e){"}\end{isabelle}%
+\isacommand{lemma}[simp]:~{"}{\isasymforall}t~e.~normal(normif~b~t~e)~=~(normal~t~{\isasymand}~normal~e){"}\end{isabelle}%
 %%% Local Variables:
 %%% mode: latex
 %%% TeX-master: "root"