src/LCF/ROOT.ML
changeset 9000 c20d58286a51
parent 6349 f7750d816c21
child 17247 6927a62c77dc
--- a/src/LCF/ROOT.ML	Tue May 30 16:03:09 2000 +0200
+++ b/src/LCF/ROOT.ML	Tue May 30 16:08:38 2000 +0200
@@ -1,9 +1,9 @@
-(*  Title:      LCF/ROOT
+(*  Title:      LCF/ROOT.ML
     ID:         $Id$
     Author:     Tobias Nipkow
     Copyright   1992  University of Cambridge
 
-Adds LCF to a database containing First-Order Logic.
+LCF on top of First-Order Logic.
 
 This theory is based on Lawrence Paulson's book Logic and Computation.
 *)