diff -r dfff821d2949 -r 59d6633835fa doc-src/TutorialI/Misc/case_exprs.thy
--- a/doc-src/TutorialI/Misc/case_exprs.thy	Mon Oct 09 09:33:45 2000 +0200
+++ b/doc-src/TutorialI/Misc/case_exprs.thy	Mon Oct 09 10:18:21 2000 +0200
@@ -65,8 +65,8 @@
 which is solved automatically:
 *}
 
-by(auto)
-
+apply(auto)
+(*<*)done(*>*)
 text{*
 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.