author  paulson 
Thu, 13 Jun 1996 16:22:37 +0200  
changeset 1793  09fff2f0d727 
parent 1613  44f5255cba9e 
child 2248  187d001fbe79 
permissions  rwrr 
1461  1 
(* Title: ZF/ex/ROOT 
0  2 
ID: $Id$ 
1461  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
0  4 
Copyright 1993 University of Cambridge 
5 

919
49271bd72c42
No longer calls maketest; instead, the Makefile writes the file
lcp
parents:
589
diff
changeset

6 
Executes miscellaneous examples for ZermeloFraenkel Set Theory 
0  7 
*) 
8 

1461  9 
ZF_build_completed; (*Make examples fail if ZF did*) 
0  10 

960
358a19a91d52
Removed exception handlers, as they are now in ZF/Makefile.
lcp
parents:
919
diff
changeset

11 
writeln"Root file for ZF Set Theory examples"; 
358a19a91d52
Removed exception handlers, as they are now in ZF/Makefile.
lcp
parents:
919
diff
changeset

12 
proof_timing := true; 
0  13 

1351  14 
time_use "misc.ML"; 
1793  15 
time_use_thy "Primes"; (*GCD theory*) 
16 
time_use_thy "Ramsey"; (*Simple form of Ramsey's theorem*) 

17 
time_use_thy "Limit"; (*Inverse limit construction of domains*) 

0  18 

960
358a19a91d52
Removed exception handlers, as they are now in ZF/Makefile.
lcp
parents:
919
diff
changeset

19 
(*Integers & Binary integer arithmetic*) 
1351  20 
time_use_thy "Bin"; 
0  21 

960
358a19a91d52
Removed exception handlers, as they are now in ZF/Makefile.
lcp
parents:
919
diff
changeset

22 
(** Datatypes **) 
1461  23 
time_use_thy "BT"; (*binary trees*) 
24 
time_use_thy "Data"; (*Sample datatype*) 

25 
time_use_thy "Term"; (*terms: recursion over the list functor*) 

26 
time_use_thy "TF"; (*trees/forests: mutual recursion*) 

27 
time_use_thy "Ntree"; (*variablebranching trees; function demo*) 

28 
time_use_thy "Brouwer"; (*Infinitebranching trees*) 

29 
time_use_thy "Enum"; (*Enormous enumeration type*) 

0  30 

960
358a19a91d52
Removed exception handlers, as they are now in ZF/Makefile.
lcp
parents:
919
diff
changeset

31 
(** Inductive definitions **) 
1461  32 
time_use_thy "Rmap"; (*mapping a relation over a list*) 
1613  33 
time_use_thy "Mutil"; (*mutilated checkerboard*) 
1461  34 
time_use_thy "PropLog"; (*completeness of propositional logic*) 
960
358a19a91d52
Removed exception handlers, as they are now in ZF/Makefile.
lcp
parents:
919
diff
changeset

35 
(*two Coq examples by Christine PaulinMohring*) 
1351  36 
time_use_thy "ListN"; 
37 
time_use_thy "Acc"; 

1461  38 
time_use_thy "Comb"; (*Combinatory Logic example*) 
39 
time_use_thy "Primrec"; (*Primitive recursive functions*) 

0  40 

960
358a19a91d52
Removed exception handlers, as they are now in ZF/Makefile.
lcp
parents:
919
diff
changeset

41 
(** CoDatatypes **) 
1351  42 
time_use_thy "LList"; 
43 
time_use_thy "CoUnit"; 

1296  44 

960
358a19a91d52
Removed exception handlers, as they are now in ZF/Makefile.
lcp
parents:
919
diff
changeset

45 
writeln"END: Root file for ZF Set Theory examples"; 