changeset 6577 | a2b5c84d590a |
parent 5377 | efb799c5ed3c |
--- 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;