author  lcp 
Wed, 17 Aug 1994 10:38:37 +0200  
changeset 540  e30c23731c2d 
parent 526  85d7ff169b9c 
child 589  31847a7504ec 
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 

540
e30c23731c2d
ZF/ex/ROOT: added .ML to use command use "ex/twos_compl"
lcp
parents:
526
diff
changeset

19 
(*Integers & Binary integer arithmetic*) 
e30c23731c2d
ZF/ex/ROOT: added .ML to use command use "ex/twos_compl"
lcp
parents:
526
diff
changeset

20 
use "ex/twos_compl.ML"; (*can delete after autoloader change 
e30c23731c2d
ZF/ex/ROOT: added .ML to use command use "ex/twos_compl"
lcp
parents:
526
diff
changeset

21 
and addition of "twos_compl" to Bin.thy*) 
515  22 
time_use_thy "ex/Bin"; 
0  23 

24 
(** Datatypes **) 

515  25 
time_use_thy "ex/BT"; (*binary trees*) 
526
85d7ff169b9c
ZF/ex/ROOT: changed "time_use" to "time_use_thy" to load CoUnit;
lcp
parents:
515
diff
changeset

26 
time_use_thy "ex/Data"; (*Sample datatype*) 
515  27 
time_use_thy "ex/Term"; (*terms: recursion over the list functor*) 
28 
time_use_thy "ex/TF"; (*trees/forests: mutual recursion*) 

489  29 
time_use_thy "ex/Ntree"; (*variablebranching trees; function demo*) 
526
85d7ff169b9c
ZF/ex/ROOT: changed "time_use" to "time_use_thy" to load CoUnit;
lcp
parents:
515
diff
changeset

30 
time_use_thy "ex/Brouwer"; (*Infinitebranching trees*) 
180
8962c2b0dc2b
ZF/ex/ROOT: changed many time_use calls to time_use_thy or else deleted
lcp
parents:
125
diff
changeset

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

33 
(** Inductive definitions **) 

180
8962c2b0dc2b
ZF/ex/ROOT: changed many time_use calls to time_use_thy or else deleted
lcp
parents:
125
diff
changeset

34 
time_use_thy "ex/Rmap"; (*mapping a relation over a list*) 
8962c2b0dc2b
ZF/ex/ROOT: changed many time_use calls to time_use_thy or else deleted
lcp
parents:
125
diff
changeset

35 
time_use_thy "ex/PropLog"; (*completeness of propositional logic*) 
515  36 
(*two Coq examples by Christine PaulinMohring*) 
180
8962c2b0dc2b
ZF/ex/ROOT: changed many time_use calls to time_use_thy or else deleted
lcp
parents:
125
diff
changeset

37 
time_use_thy "ex/ListN"; 
8962c2b0dc2b
ZF/ex/ROOT: changed many time_use calls to time_use_thy or else deleted
lcp
parents:
125
diff
changeset

38 
time_use_thy "ex/Acc"; 
515  39 
time_use_thy "ex/Comb"; (*Combinatory Logic example*) 
526
85d7ff169b9c
ZF/ex/ROOT: changed "time_use" to "time_use_thy" to load CoUnit;
lcp
parents:
515
diff
changeset

40 
time_use_thy "ex/Primrec"; (*Primitive recursive functions*) 
0  41 

120  42 
(** CoDatatypes **) 
76  43 
time_use_thy "ex/LList"; 
526
85d7ff169b9c
ZF/ex/ROOT: changed "time_use" to "time_use_thy" to load CoUnit;
lcp
parents:
515
diff
changeset

44 
time_use_thy "ex/CoUnit"; 
0  45 

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