src/ZF/Induct/ROOT.ML

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Induct/ROOT.ML	Wed Nov 07 18:12:12 2001 +0100
@@ -0,0 +1,22 @@
+(*  Title:      ZF/ex/ROOT
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   2001  University of Cambridge
+
+Inductive definitions
+*)
+
+(*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*)
+time_use_thy "ListN";
+time_use_thy "Acc";
+
+time_use_thy "Comb";            (*Combinatory Logic example*)
+time_use_thy "Primrec";         (*Primitive recursive functions*)