--- 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*)