author wenzelm
Wed, 14 Nov 2001 23:21:05 +0100
changeset 12192 6ef4ad110e90
parent 12088 6f463d16cbd0
child 12200 b544785b6cc9
permissions -rw-r--r--
removed BT, Data, Enum (see ZF/Induct);

(*  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.

time_use_thy "misc";
time_use_thy "Commutation";     (*abstract Church-Rosser theory*)
time_use_thy "Primes";          (*GCD theory*)
time_use_thy "NatSum";          (*Summing integers, squares, cubes, etc.*)
time_use_thy "Ramsey";          (*Simple form of Ramsey's theorem*)
time_use_thy "Limit";           (*Inverse limit construction of domains*)
time_use_thy "BinEx";		(*Binary integer arithmetic*)

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

(** CoDatatypes **)
time_use_thy "LList";
time_use_thy "CoUnit";