# HG changeset patch
# User wenzelm
# Date 1125762847 -7200
# Node ID 6927a62c77dc3e805b0230df5e83d09b748911f1
# Parent  0f22089c6b9e02aa858a290ecb83cad73c3b9cb0
tuned;

diff -r 0f22089c6b9e -r 6927a62c77dc src/LCF/ROOT.ML
--- a/src/LCF/ROOT.ML	Sat Sep 03 17:54:05 2005 +0200
+++ b/src/LCF/ROOT.ML	Sat Sep 03 17:54:07 2005 +0200
@@ -2,17 +2,9 @@
     ID:         $Id$
     Author:     Tobias Nipkow
     Copyright   1992  University of Cambridge
-
-LCF on top of First-Order Logic.
-
-This theory is based on Lawrence Paulson's book Logic and Computation.
 *)
 
 val banner = "Logic for Computable Functions (in FOL)";
 writeln banner;
 
-print_depth 1;
 use_thy "LCF";
-use"simpdata.ML";
-use_thy"pair";
-use_thy"fix";