src/CTT/ROOT.ML

--- a/src/CTT/ROOT.ML	Fri Sep 16 21:02:15 2005 +0200
+++ b/src/CTT/ROOT.ML	Fri Sep 16 23:01:29 2005 +0200
@@ -10,13 +10,6 @@
 val banner = "Constructive Type Theory";
 writeln banner;
 
-print_depth 1;  
-
-use_thy "CTT";
-use "~~/src/Provers/typedsimp.ML";
-use "rew.ML";
 use_thy "Main";
 
-print_depth 8;
-
 Goal "tt : T";  (*leave subgoal package empty*)