src/ZF/ex/ROOT.ML
author clasohm
Tue, 24 Oct 1995 14:50:24 +0100
changeset 1296 ae31bb7774a7
parent 1282 92543c633f20
child 1351 4a960c012383
permissions -rw-r--r--
added calls of init_html and make_chart
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
919
49271bd72c42 No longer calls maketest; instead, the Makefile writes the file
lcp
parents: 589
diff changeset
     6
Executes miscellaneous examples for Zermelo-Fraenkel Set Theory
0
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
960
358a19a91d52 Removed exception handlers, as they are now in ZF/Makefile.
lcp
parents: 919
diff changeset
    11
writeln"Root file for ZF Set Theory examples";
358a19a91d52 Removed exception handlers, as they are now in ZF/Makefile.
lcp
parents: 919
diff changeset
    12
proof_timing := true;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
960
358a19a91d52 Removed exception handlers, as they are now in ZF/Makefile.
lcp
parents: 919
diff changeset
    14
loadpath := [".", "ex"];
125
bba27d15d76e changed use_thy's parameter to exact theory name
clasohm
parents: 120
diff changeset
    15
960
358a19a91d52 Removed exception handlers, as they are now in ZF/Makefile.
lcp
parents: 919
diff changeset
    16
time_use     "ex/misc.ML";
358a19a91d52 Removed exception handlers, as they are now in ZF/Makefile.
lcp
parents: 919
diff changeset
    17
time_use_thy "ex/Ramsey";
1282
92543c633f20 Added the new Limit.{thy,ML} example
paulson
parents: 960
diff changeset
    18
time_use_thy "ex/Limit";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
960
358a19a91d52 Removed exception handlers, as they are now in ZF/Makefile.
lcp
parents: 919
diff changeset
    20
(*Integers & Binary integer arithmetic*)
358a19a91d52 Removed exception handlers, as they are now in ZF/Makefile.
lcp
parents: 919
diff changeset
    21
time_use_thy "ex/Bin";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
960
358a19a91d52 Removed exception handlers, as they are now in ZF/Makefile.
lcp
parents: 919
diff changeset
    23
(** Datatypes **)
358a19a91d52 Removed exception handlers, as they are now in ZF/Makefile.
lcp
parents: 919
diff changeset
    24
time_use_thy "ex/BT";		(*binary trees*)
358a19a91d52 Removed exception handlers, as they are now in ZF/Makefile.
lcp
parents: 919
diff changeset
    25
time_use_thy "ex/Data";		(*Sample datatype*)
358a19a91d52 Removed exception handlers, as they are now in ZF/Makefile.
lcp
parents: 919
diff changeset
    26
time_use_thy "ex/Term";		(*terms: recursion over the list functor*)
358a19a91d52 Removed exception handlers, as they are now in ZF/Makefile.
lcp
parents: 919
diff changeset
    27
time_use_thy "ex/TF";		(*trees/forests: mutual recursion*)
358a19a91d52 Removed exception handlers, as they are now in ZF/Makefile.
lcp
parents: 919
diff changeset
    28
time_use_thy "ex/Ntree";	(*variable-branching trees; function demo*)
358a19a91d52 Removed exception handlers, as they are now in ZF/Makefile.
lcp
parents: 919
diff changeset
    29
time_use_thy "ex/Brouwer";	(*Infinite-branching trees*)
358a19a91d52 Removed exception handlers, as they are now in ZF/Makefile.
lcp
parents: 919
diff changeset
    30
time_use_thy "ex/Enum";		(*Enormous enumeration type*)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
960
358a19a91d52 Removed exception handlers, as they are now in ZF/Makefile.
lcp
parents: 919
diff changeset
    32
(** Inductive definitions **)
358a19a91d52 Removed exception handlers, as they are now in ZF/Makefile.
lcp
parents: 919
diff changeset
    33
time_use_thy "ex/Rmap";		(*mapping a relation over a list*)
358a19a91d52 Removed exception handlers, as they are now in ZF/Makefile.
lcp
parents: 919
diff changeset
    34
time_use_thy "ex/PropLog";	(*completeness of propositional logic*)
358a19a91d52 Removed exception handlers, as they are now in ZF/Makefile.
lcp
parents: 919
diff changeset
    35
(*two Coq examples by Christine Paulin-Mohring*)
358a19a91d52 Removed exception handlers, as they are now in ZF/Makefile.
lcp
parents: 919
diff changeset
    36
time_use_thy "ex/ListN";
358a19a91d52 Removed exception handlers, as they are now in ZF/Makefile.
lcp
parents: 919
diff changeset
    37
time_use_thy "ex/Acc";
358a19a91d52 Removed exception handlers, as they are now in ZF/Makefile.
lcp
parents: 919
diff changeset
    38
time_use_thy "ex/Comb";		(*Combinatory Logic example*)
358a19a91d52 Removed exception handlers, as they are now in ZF/Makefile.
lcp
parents: 919
diff changeset
    39
time_use_thy "ex/Primrec";	(*Primitive recursive functions*)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
960
358a19a91d52 Removed exception handlers, as they are now in ZF/Makefile.
lcp
parents: 919
diff changeset
    41
(** CoDatatypes **)
358a19a91d52 Removed exception handlers, as they are now in ZF/Makefile.
lcp
parents: 919
diff changeset
    42
time_use_thy "ex/LList";
358a19a91d52 Removed exception handlers, as they are now in ZF/Makefile.
lcp
parents: 919
diff changeset
    43
time_use_thy "ex/CoUnit";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
1296
ae31bb7774a7 added calls of init_html and make_chart
clasohm
parents: 1282
diff changeset
    45
make_chart ();   (*make HTML chart*)
ae31bb7774a7 added calls of init_html and make_chart
clasohm
parents: 1282
diff changeset
    46
960
358a19a91d52 Removed exception handlers, as they are now in ZF/Makefile.
lcp
parents: 919
diff changeset
    47
writeln"END: Root file for ZF Set Theory examples";