author | wenzelm |
Wed, 14 Nov 2001 23:21:05 +0100 | |
changeset 12192 | 6ef4ad110e90 |
parent 12088 | 6f463d16cbd0 |
child 12200 | b544785b6cc9 |
permissions | -rw-r--r-- |
12192 | 1 |
(* Title: ZF/ex/ROOT.ML |
0 | 2 |
ID: $Id$ |
1461 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
0 | 4 |
Copyright 1993 University of Cambridge |
5 |
||
12192 | 6 |
Executes miscellaneous examples for Zermelo-Fraenkel Set Theory. |
0 | 7 |
*) |
8 |
||
11399 | 9 |
time_use_thy "misc"; |
12088 | 10 |
time_use_thy "Commutation"; (*abstract Church-Rosser theory*) |
2248 | 11 |
time_use_thy "Primes"; (*GCD theory*) |
9647 | 12 |
time_use_thy "NatSum"; (*Summing integers, squares, cubes, etc.*) |
2248 | 13 |
time_use_thy "Ramsey"; (*Simple form of Ramsey's theorem*) |
14 |
time_use_thy "Limit"; (*Inverse limit construction of domains*) |
|
11399 | 15 |
time_use_thy "BinEx"; (*Binary integer arithmetic*) |
0 | 16 |
|
960
358a19a91d52
Removed exception handlers, as they are now in ZF/Makefile.
lcp
parents:
919
diff
changeset
|
17 |
(** Datatypes **) |
1461 | 18 |
time_use_thy "Term"; (*terms: recursion over the list functor*) |
19 |
time_use_thy "TF"; (*trees/forests: mutual recursion*) |
|
20 |
time_use_thy "Ntree"; (*variable-branching trees; function demo*) |
|
21 |
time_use_thy "Brouwer"; (*Infinite-branching trees*) |
|
0 | 22 |
|
960
358a19a91d52
Removed exception handlers, as they are now in ZF/Makefile.
lcp
parents:
919
diff
changeset
|
23 |
(** CoDatatypes **) |
1351 | 24 |
time_use_thy "LList"; |
25 |
time_use_thy "CoUnit"; |