src/ZF/ex/ROOT.ML
author paulson
Fri Aug 18 12:31:20 2000 +0200 (2000-08-18)
changeset 9647 e9623f47275b
parent 9000 c20d58286a51
child 11042 bb566dd3f927
permissions -rw-r--r--
new example ZF/ex/NatSum
clasohm@1461
     1
(*  Title:      ZF/ex/ROOT
clasohm@0
     2
    ID:         $Id$
clasohm@1461
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@0
     4
    Copyright   1993  University of Cambridge
clasohm@0
     5
lcp@919
     6
Executes miscellaneous examples for Zermelo-Fraenkel Set Theory
clasohm@0
     7
*)
clasohm@0
     8
clasohm@1351
     9
time_use     "misc.ML";
paulson@2248
    10
time_use_thy "Primes";          (*GCD theory*)
paulson@9647
    11
time_use_thy "NatSum";          (*Summing integers, squares, cubes, etc.*)
paulson@2248
    12
time_use_thy "Ramsey";          (*Simple form of Ramsey's theorem*)
paulson@2248
    13
time_use_thy "Limit";           (*Inverse limit construction of domains*)
paulson@5533
    14
time_use     "BinEx";		(*Binary integer arithmetic*)
clasohm@0
    15
lcp@960
    16
(** Datatypes **)
clasohm@1461
    17
time_use_thy "BT";              (*binary trees*)
clasohm@1461
    18
time_use_thy "Data";            (*Sample datatype*)
clasohm@1461
    19
time_use_thy "Term";            (*terms: recursion over the list functor*)
clasohm@1461
    20
time_use_thy "TF";              (*trees/forests: mutual recursion*)
clasohm@1461
    21
time_use_thy "Ntree";           (*variable-branching trees; function demo*)
clasohm@1461
    22
time_use_thy "Brouwer";         (*Infinite-branching trees*)
clasohm@1461
    23
time_use_thy "Enum";            (*Enormous enumeration type*)
clasohm@0
    24
lcp@960
    25
(** Inductive definitions **)
clasohm@1461
    26
time_use_thy "Rmap";            (*mapping a relation over a list*)
paulson@6045
    27
time_use_thy "Mutil";           (*mutilated chess board*)
clasohm@1461
    28
time_use_thy "PropLog";         (*completeness of propositional logic*)
lcp@960
    29
(*two Coq examples by Christine Paulin-Mohring*)
clasohm@1351
    30
time_use_thy "ListN";
clasohm@1351
    31
time_use_thy "Acc";
clasohm@1461
    32
time_use_thy "Comb";            (*Combinatory Logic example*)
clasohm@1461
    33
time_use_thy "Primrec";         (*Primitive recursive functions*)
clasohm@0
    34
lcp@960
    35
(** CoDatatypes **)
clasohm@1351
    36
time_use_thy "LList";
clasohm@1351
    37
time_use_thy "CoUnit";