--- a/src/ZF/ex/ROOT.ML Wed Nov 14 23:20:41 2001 +0100
+++ b/src/ZF/ex/ROOT.ML Wed Nov 14 23:21:05 2001 +0100
@@ -1,9 +1,9 @@
-(* Title: ZF/ex/ROOT
+(* Title: ZF/ex/ROOT.ML
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
-Executes miscellaneous examples for Zermelo-Fraenkel Set Theory
+Executes miscellaneous examples for Zermelo-Fraenkel Set Theory.
*)
time_use_thy "misc";
@@ -15,13 +15,10 @@
time_use_thy "BinEx"; (*Binary integer arithmetic*)
(** Datatypes **)
-time_use_thy "BT"; (*binary trees*)
-time_use_thy "Data"; (*Sample datatype*)
time_use_thy "Term"; (*terms: recursion over the list functor*)
time_use_thy "TF"; (*trees/forests: mutual recursion*)
time_use_thy "Ntree"; (*variable-branching trees; function demo*)
time_use_thy "Brouwer"; (*Infinite-branching trees*)
-time_use_thy "Enum"; (*Enormous enumeration type*)
(** CoDatatypes **)
time_use_thy "LList";