src/ZF/ROOT.ML
changeset 16483 ace3c2b95353
parent 15481 fc075ae929e4
child 17935 c6f1442ce949
     1.1 --- a/src/ZF/ROOT.ML	Mon Jun 20 22:13:55 2005 +0200
     1.2 +++ b/src/ZF/ROOT.ML	Mon Jun 20 22:13:56 2005 +0200
     1.3 @@ -13,13 +13,9 @@
     1.4  
     1.5  reset eta_contract;
     1.6  
     1.7 -print_depth 1;
     1.8 -
     1.9  (*syntax for old-style theory sections*)
    1.10  use "thy_syntax";
    1.11  
    1.12  with_path "Integ" use_thy "Main_ZFC";
    1.13  
    1.14 -print_depth 8;
    1.15 -
    1.16  Goal "True";  (*leave subgoal package empty*)