author  wenzelm 
Wed, 14 Nov 2001 23:21:05 +0100  
changeset 12192  6ef4ad110e90 
parent 12088  6f463d16cbd0 
child 12200  b544785b6cc9 
permissions  rwrr 
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 ZermeloFraenkel Set Theory. 
0  7 
*) 
8 

11399  9 
time_use_thy "misc"; 
12088  10 
time_use_thy "Commutation"; (*abstract ChurchRosser 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"; (*variablebranching trees; function demo*) 

21 
time_use_thy "Brouwer"; (*Infinitebranching 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"; 