--- 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
(*>*)