author  clasohm 
Tue, 16 Nov 1993 14:26:15 +0100  
changeset 125  bba27d15d76e 
parent 120  09287f26bfb8 
child 180  8962c2b0dc2b 
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 

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

0  16 
time_use "ex/misc.ML"; 
125  17 
time_use_thy "ex/Ramsey"; 
0  18 

19 
(*Equivalence classes and integers*) 

125  20 
time_use_thy "ex/Equiv"; 
21 
time_use_thy "ex/Integ"; 

0  22 
(*Binary integer arithmetic*) 
91  23 
use "ex/twos_compl.ML"; 
0  24 
time_use "ex/bin.ML"; 
125  25 
time_use_thy "ex/BinFn"; 
0  26 

27 
(** Datatypes **) 

28 
(*binary trees*) 

29 
time_use "ex/bt.ML"; 

125  30 
time_use_thy "ex/BT_Fn"; 
0  31 
(*terms: recursion over the list functor*) 
32 
time_use "ex/term.ML"; 

125  33 
time_use_thy "ex/TermFn"; 
0  34 
(*trees/forests: mutual recursion*) 
35 
time_use "ex/tf.ML"; 

125  36 
time_use_thy "ex/TF_Fn"; 
56  37 
(*Sample datatype; enormous enumeration type*) 
38 
time_use "ex/data.ML"; 

0  39 
time_use "ex/enum.ML"; 
40 

41 
(** Inductive definitions **) 

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

42 
(*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

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

125  46 
time_use_thy "ex/PropLog"; 
0  47 
(*two Coq examples by Ch. PaulinMohring*) 
48 
time_use "ex/listn.ML"; 

49 
time_use "ex/acc.ML"; 

50 
(*Diamond property for combinatory logic*) 

51 
time_use "ex/comb.ML"; 

125  52 
time_use_thy "ex/Contract0"; 
0  53 
time_use "ex/parcontract.ML"; 
125  54 
time_use_thy "ex/Primrec0"; 
0  55 

120  56 
(** CoDatatypes **) 
76  57 
time_use_thy "ex/LList"; 
34
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
16
diff
changeset

58 
time_use "ex/llist_eq.ML"; 
125  59 
time_use_thy "ex/LListFn"; 
95  60 
time_use "ex/counit.ML"; 
0  61 

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