src/FOL/ex/ROOT.ML
changeset 11675 c87d695f4adb
parent 9205 f171fa6a0989
child 12369 ab207f9c1e1e
--- a/src/FOL/ex/ROOT.ML	Thu Oct 04 15:25:51 2001 +0200
+++ b/src/FOL/ex/ROOT.ML	Thu Oct 04 15:26:14 2001 +0200
@@ -1,13 +1,14 @@
-(*  Title:      FOL/ex/ROOT
+(*  Title:      FOL/ex/ROOT.ML
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
 
-Executes all examples for First-Order Logic. 
+Examples for First-Order Logic. 
 *)
 
 time_use     "intro.ML";
 time_use_thy "Nat";
+time_use_thy "Natural_Numbers";
 time_use     "foundn.ML";
 time_use_thy "Prolog";