removed obsolete print_depth;
authorwenzelm
Mon Jun 20 22:13:56 2005 +0200 (2005-06-20)
changeset 16483ace3c2b95353
parent 16482 ed08c8edc289
child 16484 eaf7bb77fed6
removed obsolete print_depth;
src/FOL/ROOT.ML
src/HOL/ROOT.ML
src/HOLCF/ROOT.ML
src/ZF/ROOT.ML
     1.1 --- a/src/FOL/ROOT.ML	Mon Jun 20 22:13:55 2005 +0200
     1.2 +++ b/src/FOL/ROOT.ML	Mon Jun 20 22:13:56 2005 +0200
     1.3 @@ -8,8 +8,6 @@
     1.4  
     1.5  writeln banner;
     1.6  
     1.7 -print_depth 1;  
     1.8 -
     1.9  use "~~/src/Provers/splitter.ML";
    1.10  use "~~/src/Provers/ind.ML";
    1.11  use "~~/src/Provers/hypsubst.ML";
    1.12 @@ -21,5 +19,3 @@
    1.13  use "~~/src/Provers/quantifier1.ML";
    1.14  
    1.15  use_thy "FOL";
    1.16 -
    1.17 -print_depth 8;
     2.1 --- a/src/HOL/ROOT.ML	Mon Jun 20 22:13:55 2005 +0200
     2.2 +++ b/src/HOL/ROOT.ML	Mon Jun 20 22:13:56 2005 +0200
     2.3 @@ -9,8 +9,6 @@
     2.4  val banner = "Higher-Order Logic";
     2.5  writeln banner;
     2.6  
     2.7 -print_depth 1;
     2.8 -
     2.9  (*old-style theory syntax*)
    2.10  use "thy_syntax.ML";
    2.11  
    2.12 @@ -40,8 +38,6 @@
    2.13  
    2.14  path_add "~~/src/HOL/Library";
    2.15  
    2.16 -print_depth 8;
    2.17 -
    2.18  Goal "True";  (*leave subgoal package empty*)
    2.19  
    2.20  val HOL_proofs = !proofs;
     3.1 --- a/src/HOLCF/ROOT.ML	Mon Jun 20 22:13:55 2005 +0200
     3.2 +++ b/src/HOLCF/ROOT.ML	Mon Jun 20 22:13:56 2005 +0200
     3.3 @@ -8,8 +8,6 @@
     3.4  val banner = "HOLCF";
     3.5  writeln banner;
     3.6  
     3.7 -print_depth 1;
     3.8 -
     3.9  use_thy "HOLCF";
    3.10  
    3.11  use "holcf_logic.ML";
    3.12 @@ -24,5 +22,3 @@
    3.13  use "domain/interface.ML";
    3.14  
    3.15  path_add "~~/src/HOLCF/ex";
    3.16 -
    3.17 -print_depth 10;  
     4.1 --- a/src/ZF/ROOT.ML	Mon Jun 20 22:13:55 2005 +0200
     4.2 +++ b/src/ZF/ROOT.ML	Mon Jun 20 22:13:56 2005 +0200
     4.3 @@ -13,13 +13,9 @@
     4.4  
     4.5  reset eta_contract;
     4.6  
     4.7 -print_depth 1;
     4.8 -
     4.9  (*syntax for old-style theory sections*)
    4.10  use "thy_syntax";
    4.11  
    4.12  with_path "Integ" use_thy "Main_ZFC";
    4.13  
    4.14 -print_depth 8;
    4.15 -
    4.16  Goal "True";  (*leave subgoal package empty*)