diff -r 7e0b35bed503 -r a2b5c84d590a doc-src/Tutorial/Misc/ROOT.ML
--- a/doc-src/Tutorial/Misc/ROOT.ML	Tue May 04 16:18:16 1999 +0200
+++ b/doc-src/Tutorial/Misc/ROOT.ML	Tue May 04 16:49:24 1999 +0200
@@ -1,3 +1,11 @@
+context Main.thy;
+use "arith1.ML";
+by(Auto_tac);
+use "arith2.ML";
+by(arith_tac 1);
+use "arith3.ML";
+by(arith_tac 1);
+
 use_thy "Tree";
 
 context Main.thy;