# HG changeset patch
# User wenzelm
# Date 1005776414 -3600
# Node ID 32a9c240f225094f0172ac03c83b93abbbb79d4f
# Parent  4729bbf86626a63fd3a995078c95cac9ac2dd5ec
added Datatypes, Binary_Trees (from ZF/ex);

diff -r 4729bbf86626 -r 32a9c240f225 src/ZF/Induct/ROOT.ML
--- a/src/ZF/Induct/ROOT.ML	Wed Nov 14 23:19:09 2001 +0100
+++ b/src/ZF/Induct/ROOT.ML	Wed Nov 14 23:20:14 2001 +0100
@@ -6,12 +6,14 @@
 Inductive definitions
 *)
 
+time_use_thy "Datatypes";
+time_use_thy "Binary_Trees";
+time_use_thy "Mutil";           (*mutilated chess board*)
+
 (*by Sidi Ehmety: Multisets.  A parent is FoldSet, the "fold" function for
 finite sets*)
 time_use_thy "Multiset";
-
 time_use_thy "Rmap";            (*mapping a relation over a list*)
-time_use_thy "Mutil";           (*mutilated chess board*)
 time_use_thy "PropLog";         (*completeness of propositional logic*)
 
 (*two Coq examples by Christine Paulin-Mohring*)