--- 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"