# HG changeset patch
# User wenzelm
# Date 1005776465 -3600
# Node ID 6ef4ad110e90830a5ef3d42c51403e796fea3844
# Parent  2c383ee7ff16383b38df33fd47fc910a9f01c403
removed BT, Data, Enum (see ZF/Induct);

diff -r 2c383ee7ff16 -r 6ef4ad110e90 src/ZF/ex/ROOT.ML
--- 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";