author  clasohm 
Tue, 24 Oct 1995 14:50:24 +0100  
changeset 1296  ae31bb7774a7 
parent 1282  92543c633f20 
child 1351  4a960c012383 
permissions  rwrr 
0  1 
(* Title: ZF/ex/ROOT 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

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 

16
0b033d50ca1c
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
0
diff
changeset

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 

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

14 
loadpath := [".", "ex"]; 
125  15 

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

16 
time_use "ex/misc.ML"; 
358a19a91d52
Removed exception handlers, as they are now in ZF/Makefile.
lcp
parents:
919
diff
changeset

17 
time_use_thy "ex/Ramsey"; 
1282  18 
time_use_thy "ex/Limit"; 
0  19 

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

20 
(*Integers & Binary integer arithmetic*) 
358a19a91d52
Removed exception handlers, as they are now in ZF/Makefile.
lcp
parents:
919
diff
changeset

21 
time_use_thy "ex/Bin"; 
0  22 

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

23 
(** Datatypes **) 
358a19a91d52
Removed exception handlers, as they are now in ZF/Makefile.
lcp
parents:
919
diff
changeset

24 
time_use_thy "ex/BT"; (*binary trees*) 
358a19a91d52
Removed exception handlers, as they are now in ZF/Makefile.
lcp
parents:
919
diff
changeset

25 
time_use_thy "ex/Data"; (*Sample datatype*) 
358a19a91d52
Removed exception handlers, as they are now in ZF/Makefile.
lcp
parents:
919
diff
changeset

26 
time_use_thy "ex/Term"; (*terms: recursion over the list functor*) 
358a19a91d52
Removed exception handlers, as they are now in ZF/Makefile.
lcp
parents:
919
diff
changeset

27 
time_use_thy "ex/TF"; (*trees/forests: mutual recursion*) 
358a19a91d52
Removed exception handlers, as they are now in ZF/Makefile.
lcp
parents:
919
diff
changeset

28 
time_use_thy "ex/Ntree"; (*variablebranching trees; function demo*) 
358a19a91d52
Removed exception handlers, as they are now in ZF/Makefile.
lcp
parents:
919
diff
changeset

29 
time_use_thy "ex/Brouwer"; (*Infinitebranching trees*) 
358a19a91d52
Removed exception handlers, as they are now in ZF/Makefile.
lcp
parents:
919
diff
changeset

30 
time_use_thy "ex/Enum"; (*Enormous enumeration type*) 
0  31 

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

32 
(** Inductive definitions **) 
358a19a91d52
Removed exception handlers, as they are now in ZF/Makefile.
lcp
parents:
919
diff
changeset

33 
time_use_thy "ex/Rmap"; (*mapping a relation over a list*) 
358a19a91d52
Removed exception handlers, as they are now in ZF/Makefile.
lcp
parents:
919
diff
changeset

34 
time_use_thy "ex/PropLog"; (*completeness of propositional logic*) 
358a19a91d52
Removed exception handlers, as they are now in ZF/Makefile.
lcp
parents:
919
diff
changeset

35 
(*two Coq examples by Christine PaulinMohring*) 
358a19a91d52
Removed exception handlers, as they are now in ZF/Makefile.
lcp
parents:
919
diff
changeset

36 
time_use_thy "ex/ListN"; 
358a19a91d52
Removed exception handlers, as they are now in ZF/Makefile.
lcp
parents:
919
diff
changeset

37 
time_use_thy "ex/Acc"; 
358a19a91d52
Removed exception handlers, as they are now in ZF/Makefile.
lcp
parents:
919
diff
changeset

38 
time_use_thy "ex/Comb"; (*Combinatory Logic example*) 
358a19a91d52
Removed exception handlers, as they are now in ZF/Makefile.
lcp
parents:
919
diff
changeset

39 
time_use_thy "ex/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 **) 
358a19a91d52
Removed exception handlers, as they are now in ZF/Makefile.
lcp
parents:
919
diff
changeset

42 
time_use_thy "ex/LList"; 
358a19a91d52
Removed exception handlers, as they are now in ZF/Makefile.
lcp
parents:
919
diff
changeset

43 
time_use_thy "ex/CoUnit"; 
0  44 

1296  45 
make_chart (); (*make HTML chart*) 
46 

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

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