--- a/src/FOL/ROOT.ML Mon Jun 20 22:13:55 2005 +0200
+++ b/src/FOL/ROOT.ML Mon Jun 20 22:13:56 2005 +0200
@@ -8,8 +8,6 @@
writeln banner;
-print_depth 1;
-
use "~~/src/Provers/splitter.ML";
use "~~/src/Provers/ind.ML";
use "~~/src/Provers/hypsubst.ML";
@@ -21,5 +19,3 @@
use "~~/src/Provers/quantifier1.ML";
use_thy "FOL";
-
-print_depth 8;
--- a/src/HOL/ROOT.ML Mon Jun 20 22:13:55 2005 +0200
+++ b/src/HOL/ROOT.ML Mon Jun 20 22:13:56 2005 +0200
@@ -9,8 +9,6 @@
val banner = "Higher-Order Logic";
writeln banner;
-print_depth 1;
-
(*old-style theory syntax*)
use "thy_syntax.ML";
@@ -40,8 +38,6 @@
path_add "~~/src/HOL/Library";
-print_depth 8;
-
Goal "True"; (*leave subgoal package empty*)
val HOL_proofs = !proofs;
--- a/src/HOLCF/ROOT.ML Mon Jun 20 22:13:55 2005 +0200
+++ b/src/HOLCF/ROOT.ML Mon Jun 20 22:13:56 2005 +0200
@@ -8,8 +8,6 @@
val banner = "HOLCF";
writeln banner;
-print_depth 1;
-
use_thy "HOLCF";
use "holcf_logic.ML";
@@ -24,5 +22,3 @@
use "domain/interface.ML";
path_add "~~/src/HOLCF/ex";
-
-print_depth 10;
--- 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*)