author  lcp 
Fri, 15 Oct 1993 10:25:23 +0100  
changeset 56  2caa6f49f06e 
parent 34  747f1aad03cf 
child 76  c616d66c640e 
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 

6 
Executes all examples for ZermeloFraenkel Set Theory 

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 

11 
writeln"Root file for ZF Set Theory examples"; 

12 
proof_timing := true; 

13 

14 
time_use "ex/misc.ML"; 

15 
time_use_thy "ex/ramsey"; 

16 

17 
(*Equivalence classes and integers*) 

18 
time_use_thy "ex/equiv"; 

19 
time_use_thy "ex/integ"; 

20 
(*Binary integer arithmetic*) 

21 
use "ex/twoscompl.ML"; 

22 
time_use "ex/bin.ML"; 

34
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
16
diff
changeset

23 
time_use_thy "ex/binfn"; 
0  24 

25 
(** Datatypes **) 

26 
(*binary trees*) 

27 
time_use "ex/bt.ML"; 

34
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
16
diff
changeset

28 
time_use_thy "ex/bt_fn"; 
0  29 
(*terms: recursion over the list functor*) 
30 
time_use "ex/term.ML"; 

34
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
16
diff
changeset

31 
time_use_thy "ex/termfn"; 
0  32 
(*trees/forests: mutual recursion*) 
33 
time_use "ex/tf.ML"; 

34
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
16
diff
changeset

34 
time_use_thy "ex/tf_fn"; 
56  35 
(*Sample datatype; enormous enumeration type*) 
36 
time_use "ex/data.ML"; 

0  37 
time_use "ex/enum.ML"; 
38 

39 
(** Inductive definitions **) 

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

40 
(*mapping a relation over a list*) 
0b033d50ca1c
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
0
diff
changeset

41 
time_use "ex/rmap.ML"; 
0  42 
(*completeness of propositional logic*) 
43 
time_use "ex/prop.ML"; 

34
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
16
diff
changeset

44 
time_use_thy "ex/propthms"; 
0  45 
(*two Coq examples by Ch. PaulinMohring*) 
46 
time_use "ex/listn.ML"; 

47 
time_use "ex/acc.ML"; 

48 
(*Diamond property for combinatory logic*) 

49 
time_use "ex/comb.ML"; 

50 
time_use_thy "ex/contract"; 

51 
time_use "ex/parcontract.ML"; 

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

52 
time_use_thy "ex/primrec"; 
0  53 

54 
(** CoDatatypes **) 

55 
time_use "ex/llist.ML"; 

34
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
16
diff
changeset

56 
time_use "ex/llist_eq.ML"; 
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
16
diff
changeset

57 
time_use_thy "ex/llistfn"; 
0  58 

59 

60 
maketest"END: Root file for ZF Set Theory examples"; 