author  lcp 
Thu, 30 Sep 1993 10:54:01 +0100  
changeset 16  0b033d50ca1c 
parent 0  a5a9c433f639 
child 34  747f1aad03cf 
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"; 

23 
time_use_thy "ex/binfn"; 

24 

25 
(** Datatypes **) 

26 
(*binary trees*) 

27 
time_use "ex/bt.ML"; 

28 
time_use_thy "ex/btfn"; 

29 
(*terms: recursion over the list functor*) 

30 
time_use "ex/term.ML"; 

31 
time_use_thy "ex/termfn"; 

32 
(*trees/forests: mutual recursion*) 

33 
time_use "ex/tf.ML"; 

34 
time_use_thy "ex/tffn"; 

35 
(*Enormous enumeration type  could be even bigger?*) 

36 
time_use "ex/enum.ML"; 

37 

38 
(** Inductive definitions **) 

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

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

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

43 
time_use_thy "ex/proplog"; 

44 
(*two Coq examples by Ch. PaulinMohring*) 

45 
time_use "ex/listn.ML"; 

46 
time_use "ex/acc.ML"; 

47 
(*Diamond property for combinatory logic*) 

48 
time_use "ex/comb.ML"; 

49 
time_use_thy "ex/contract"; 

50 
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

51 
time_use_thy "ex/primrec"; 
0  52 

53 
(** CoDatatypes **) 

54 
time_use "ex/llist.ML"; 

55 
time_use_thy "ex/llistfn"; 

56 

57 

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