| author | wenzelm |
| Tue, 04 Jul 2006 19:49:49 +0200 | |
| changeset 19998 | c8018518e112 |
| parent 14883 | ca000a495448 |
| child 23912 | 039ae566a4a2 |
| 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"; |
| 14883 | 10 |
time_use_thy "Ring"; (*abstract algebra*) |
| 12088 | 11 |
time_use_thy "Commutation"; (*abstract Church-Rosser theory*) |
| 2248 | 12 |
time_use_thy "Primes"; (*GCD theory*) |
| 9647 | 13 |
time_use_thy "NatSum"; (*Summing integers, squares, cubes, etc.*) |
| 2248 | 14 |
time_use_thy "Ramsey"; (*Simple form of Ramsey's theorem*) |
15 |
time_use_thy "Limit"; (*Inverse limit construction of domains*) |
|
| 11399 | 16 |
time_use_thy "BinEx"; (*Binary integer arithmetic*) |
| 0 | 17 |
|
|
960
358a19a91d52
Removed exception handlers, as they are now in ZF/Makefile.
lcp
parents:
919
diff
changeset
|
18 |
(** CoDatatypes **) |
| 1351 | 19 |
time_use_thy "LList"; |
20 |
time_use_thy "CoUnit"; |