diff -r 3566c197b420 -r a58082b8066c src/CCL/ROOT.ML --- a/src/CCL/ROOT.ML Thu Apr 06 10:48:11 1995 +0200 +++ b/src/CCL/ROOT.ML Thu Apr 06 10:49:53 1995 +0200 @@ -7,6 +7,10 @@ *) val banner = "Classical Computational Logic (in FOL)"; +writeln banner; + +print_depth 1; +set eta_contract; (* Higher-Order Set Theory Extension to FOL *) (* used as basis for CCL *) @@ -34,4 +38,6 @@ use "eval.ML"; use_thy "Fix"; +print_depth 8; + val CCL_build_completed = (); (*indicate successful build*)