diff -r dfff821d2949 -r 59d6633835fa doc-src/TutorialI/Misc/document/case_exprs.tex
--- a/doc-src/TutorialI/Misc/document/case_exprs.tex	Mon Oct 09 09:33:45 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/case_exprs.tex	Mon Oct 09 10:18:21 2000 +0200
@@ -71,7 +71,7 @@
 \end{isabelle}
 which is solved automatically:%
 \end{isamarkuptxt}%
-\isacommand{by}{\isacharparenleft}auto{\isacharparenright}%
+\isacommand{apply}{\isacharparenleft}auto{\isacharparenright}%
 \begin{isamarkuptext}%
 Note that we do not need to give a lemma a name if we do not intend to refer
 to it explicitly in the future.%