diff -r 966974a7a5b3 -r c613cd06d5cf doc-src/TutorialI/Misc/Tree.thy
--- a/doc-src/TutorialI/Misc/Tree.thy	Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/Misc/Tree.thy	Fri Jul 28 16:02:51 2000 +0200
@@ -21,7 +21,7 @@
 lemma mirror_mirror: "mirror(mirror t) = t";
 (*<*)
 apply(induct_tac t);
-apply(auto).;
+by(auto);
 
 end
 (*>*)