(* Title: ZF/Induct/ROOT.ML
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 2001 University of Cambridge
Inductive definitions.
*)
time_use_thy "Datatypes";
time_use_thy "Binary_Trees";
time_use_thy "Term"; (*recursion over the list functor*)
time_use_thy "Tree_Forest"; (*mutual recursion*)
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 "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*)