src/ZF/ex/ROOT.ML
author clasohm
Tue, 16 Nov 1993 14:26:15 +0100
changeset 125 bba27d15d76e
parent 120 09287f26bfb8
child 180 8962c2b0dc2b
permissions -rw-r--r--
changed use_thy's parameter to exact theory name
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     1
(*  Title: 	ZF/ex/ROOT
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1993  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
Executes all examples for Zermelo-Fraenkel Set Theory
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     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
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
writeln"Root file for ZF Set Theory examples";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
proof_timing := true;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
125
bba27d15d76e changed use_thy's parameter to exact theory name
clasohm
parents: 120
diff changeset
    14
loadpath := [".", "ex"];
bba27d15d76e changed use_thy's parameter to exact theory name
clasohm
parents: 120
diff changeset
    15
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
time_use     "ex/misc.ML";
125
bba27d15d76e changed use_thy's parameter to exact theory name
clasohm
parents: 120
diff changeset
    17
time_use_thy "ex/Ramsey";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
(*Equivalence classes and integers*)
125
bba27d15d76e changed use_thy's parameter to exact theory name
clasohm
parents: 120
diff changeset
    20
time_use_thy "ex/Equiv";
bba27d15d76e changed use_thy's parameter to exact theory name
clasohm
parents: 120
diff changeset
    21
time_use_thy "ex/Integ";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
(*Binary integer arithmetic*)
91
30c8e9c380a2 renamed twos-compl.ML to twos_compl.ML
clasohm
parents: 76
diff changeset
    23
use          "ex/twos_compl.ML";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
time_use     "ex/bin.ML";
125
bba27d15d76e changed use_thy's parameter to exact theory name
clasohm
parents: 120
diff changeset
    25
time_use_thy "ex/BinFn";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
(** Datatypes **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
(*binary trees*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
time_use     "ex/bt.ML";
125
bba27d15d76e changed use_thy's parameter to exact theory name
clasohm
parents: 120
diff changeset
    30
time_use_thy "ex/BT_Fn";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
(*terms: recursion over the list functor*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
time_use     "ex/term.ML";
125
bba27d15d76e changed use_thy's parameter to exact theory name
clasohm
parents: 120
diff changeset
    33
time_use_thy "ex/TermFn";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
(*trees/forests: mutual recursion*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
time_use     "ex/tf.ML";
125
bba27d15d76e changed use_thy's parameter to exact theory name
clasohm
parents: 120
diff changeset
    36
time_use_thy "ex/TF_Fn";
56
2caa6f49f06e ZF/ex/tf/tree,forest_unfold: streamlined the proofs
lcp
parents: 34
diff changeset
    37
(*Sample datatype; enormous enumeration type*)
2caa6f49f06e ZF/ex/tf/tree,forest_unfold: streamlined the proofs
lcp
parents: 34
diff changeset
    38
time_use     "ex/data.ML";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
time_use     "ex/enum.ML";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    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
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
(*completeness of propositional logic*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
time_use     "ex/prop.ML";
125
bba27d15d76e changed use_thy's parameter to exact theory name
clasohm
parents: 120
diff changeset
    46
time_use_thy "ex/PropLog";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
(*two Coq examples by Ch. Paulin-Mohring*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
time_use     "ex/listn.ML";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    49
time_use     "ex/acc.ML";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    50
(*Diamond property for combinatory logic*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
time_use     "ex/comb.ML";
125
bba27d15d76e changed use_thy's parameter to exact theory name
clasohm
parents: 120
diff changeset
    52
time_use_thy "ex/Contract0";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
time_use     "ex/parcontract.ML";
125
bba27d15d76e changed use_thy's parameter to exact theory name
clasohm
parents: 120
diff changeset
    54
time_use_thy "ex/Primrec0";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    55
120
09287f26bfb8 changed all co- and co_ to co
lcp
parents: 95
diff changeset
    56
(** CoDatatypes **)
76
c616d66c640e renamed some files
clasohm
parents: 56
diff changeset
    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
bba27d15d76e changed use_thy's parameter to exact theory name
clasohm
parents: 120
diff changeset
    59
time_use_thy "ex/LListFn";
95
2246a80b1cb5 Minor changes; addition of counit.ML
lcp
parents: 91
diff changeset
    60
time_use     "ex/counit.ML";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    61
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    62
maketest"END: Root file for ZF Set Theory examples";