src/ZF/ex/ROOT.ML
author paulson
Tue, 26 Mar 1996 12:01:13 +0100
changeset 1613 44f5255cba9e
parent 1461 6bcb44e4d6e5
child 1793 09fff2f0d727
permissions -rw-r--r--
Now loads Mutil example
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1351
diff changeset
     1
(*  Title:      ZF/ex/ROOT
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1351
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
0
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
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1351
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
1351
4a960c012383 removed make_chart;
clasohm
parents: 1296
diff changeset
    14
time_use     "misc.ML";
4a960c012383 removed make_chart;
clasohm
parents: 1296
diff changeset
    15
time_use_thy "Ramsey";
4a960c012383 removed make_chart;
clasohm
parents: 1296
diff changeset
    16
time_use_thy "Limit";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
960
358a19a91d52 Removed exception handlers, as they are now in ZF/Makefile.
lcp
parents: 919
diff changeset
    18
(*Integers & Binary integer arithmetic*)
1351
4a960c012383 removed make_chart;
clasohm
parents: 1296
diff changeset
    19
time_use_thy "Bin";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
960
358a19a91d52 Removed exception handlers, as they are now in ZF/Makefile.
lcp
parents: 919
diff changeset
    21
(** Datatypes **)
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1351
diff changeset
    22
time_use_thy "BT";              (*binary trees*)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1351
diff changeset
    23
time_use_thy "Data";            (*Sample datatype*)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1351
diff changeset
    24
time_use_thy "Term";            (*terms: recursion over the list functor*)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1351
diff changeset
    25
time_use_thy "TF";              (*trees/forests: mutual recursion*)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1351
diff changeset
    26
time_use_thy "Ntree";           (*variable-branching trees; function demo*)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1351
diff changeset
    27
time_use_thy "Brouwer";         (*Infinite-branching trees*)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1351
diff changeset
    28
time_use_thy "Enum";            (*Enormous enumeration type*)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
960
358a19a91d52 Removed exception handlers, as they are now in ZF/Makefile.
lcp
parents: 919
diff changeset
    30
(** Inductive definitions **)
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1351
diff changeset
    31
time_use_thy "Rmap";            (*mapping a relation over a list*)
1613
44f5255cba9e Now loads Mutil example
paulson
parents: 1461
diff changeset
    32
time_use_thy "Mutil";           (*mutilated checkerboard*)
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1351
diff changeset
    33
time_use_thy "PropLog";         (*completeness of propositional logic*)
960
358a19a91d52 Removed exception handlers, as they are now in ZF/Makefile.
lcp
parents: 919
diff changeset
    34
(*two Coq examples by Christine Paulin-Mohring*)
1351
4a960c012383 removed make_chart;
clasohm
parents: 1296
diff changeset
    35
time_use_thy "ListN";
4a960c012383 removed make_chart;
clasohm
parents: 1296
diff changeset
    36
time_use_thy "Acc";
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1351
diff changeset
    37
time_use_thy "Comb";            (*Combinatory Logic example*)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1351
diff changeset
    38
time_use_thy "Primrec";         (*Primitive recursive functions*)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
960
358a19a91d52 Removed exception handlers, as they are now in ZF/Makefile.
lcp
parents: 919
diff changeset
    40
(** CoDatatypes **)
1351
4a960c012383 removed make_chart;
clasohm
parents: 1296
diff changeset
    41
time_use_thy "LList";
4a960c012383 removed make_chart;
clasohm
parents: 1296
diff changeset
    42
time_use_thy "CoUnit";
1296
ae31bb7774a7 added calls of init_html and make_chart
clasohm
parents: 1282
diff changeset
    43
960
358a19a91d52 Removed exception handlers, as they are now in ZF/Makefile.
lcp
parents: 919
diff changeset
    44
writeln"END: Root file for ZF Set Theory examples";