src/ZF/ROOT.ML
changeset 16483 ace3c2b95353
parent 15481 fc075ae929e4
child 17935 c6f1442ce949
--- a/src/ZF/ROOT.ML	Mon Jun 20 22:13:55 2005 +0200
+++ b/src/ZF/ROOT.ML	Mon Jun 20 22:13:56 2005 +0200
@@ -13,13 +13,9 @@
 
 reset eta_contract;
 
-print_depth 1;
-
 (*syntax for old-style theory sections*)
 use "thy_syntax";
 
 with_path "Integ" use_thy "Main_ZFC";
 
-print_depth 8;
-
 Goal "True";  (*leave subgoal package empty*)