# HG changeset patch
# User wenzelm
# Date 1180628207 -7200
# Node ID cd928fd965a8efcd09c1ef069f2444b780f27926
# Parent  b7d0e78be86d595dc12e6e4b3133b05211170dcb
tuned header;

diff -r b7d0e78be86d -r cd928fd965a8 src/FOL/ROOT.ML
--- a/src/FOL/ROOT.ML	Thu May 31 18:16:46 2007 +0200
+++ b/src/FOL/ROOT.ML	Thu May 31 18:16:47 2007 +0200
@@ -1,10 +1,7 @@
 (*  Title:      FOL/ROOT.ML
     ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1993  University of Cambridge
+
+First-Order Logic with Natural Deduction.
 *)
 
-val banner = "First-Order Logic with Natural Deduction";
-writeln banner;
-
 use_thy "FOL";