author | wenzelm |
Tue, 30 May 2000 16:08:38 +0200 | |
changeset 9000 | c20d58286a51 |
parent 6349 | f7750d816c21 |
child 9647 | e9623f47275b |
permissions | -rw-r--r-- |
1461 | 1 |
(* Title: ZF/ex/ROOT |
0 | 2 |
ID: $Id$ |
1461 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
0 | 4 |
Copyright 1993 University of Cambridge |
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 | 7 |
*) |
8 |
||
1351 | 9 |
time_use "misc.ML"; |
2248 | 10 |
time_use_thy "Primes"; (*GCD theory*) |
11 |
time_use_thy "Ramsey"; (*Simple form of Ramsey's theorem*) |
|
12 |
time_use_thy "Limit"; (*Inverse limit construction of domains*) |
|
5533 | 13 |
time_use "BinEx"; (*Binary integer arithmetic*) |
0 | 14 |
|
960
358a19a91d52
Removed exception handlers, as they are now in ZF/Makefile.
lcp
parents:
919
diff
changeset
|
15 |
(** Datatypes **) |
1461 | 16 |
time_use_thy "BT"; (*binary trees*) |
17 |
time_use_thy "Data"; (*Sample datatype*) |
|
18 |
time_use_thy "Term"; (*terms: recursion over the list functor*) |
|
19 |
time_use_thy "TF"; (*trees/forests: mutual recursion*) |
|
20 |
time_use_thy "Ntree"; (*variable-branching trees; function demo*) |
|
21 |
time_use_thy "Brouwer"; (*Infinite-branching trees*) |
|
22 |
time_use_thy "Enum"; (*Enormous enumeration type*) |
|
0 | 23 |
|
960
358a19a91d52
Removed exception handlers, as they are now in ZF/Makefile.
lcp
parents:
919
diff
changeset
|
24 |
(** Inductive definitions **) |
1461 | 25 |
time_use_thy "Rmap"; (*mapping a relation over a list*) |
6045 | 26 |
time_use_thy "Mutil"; (*mutilated chess board*) |
1461 | 27 |
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
|
28 |
(*two Coq examples by Christine Paulin-Mohring*) |
1351 | 29 |
time_use_thy "ListN"; |
30 |
time_use_thy "Acc"; |
|
1461 | 31 |
time_use_thy "Comb"; (*Combinatory Logic example*) |
32 |
time_use_thy "Primrec"; (*Primitive recursive functions*) |
|
0 | 33 |
|
960
358a19a91d52
Removed exception handlers, as they are now in ZF/Makefile.
lcp
parents:
919
diff
changeset
|
34 |
(** CoDatatypes **) |
1351 | 35 |
time_use_thy "LList"; |
36 |
time_use_thy "CoUnit"; |