author | nipkow |
Fri, 29 Nov 1996 15:08:06 +0100 | |
changeset 2280 | eb2ba30c2981 |
parent 2222 | a3fb552f10e3 |
child 2987 | becc227bad4d |
permissions | -rw-r--r-- |
1465 | 1 |
(* Title: HOL/ex/ROOT |
969 | 2 |
ID: $Id$ |
1465 | 3 |
Author: Tobias Nipkow, Cambridge University Computer Laboratory |
969 | 4 |
Copyright 1991 University of Cambridge |
5 |
||
6 |
Executes miscellaneous examples for Higher-Order Logic. |
|
7 |
*) |
|
8 |
||
1165 | 9 |
HOL_build_completed; (*Cause examples to fail if HOL did*) |
969 | 10 |
|
1165 | 11 |
writeln "Root file for HOL examples"; |
1026
f2dc38ed53ac
ROOT.ML: Removed the "exit 1" calls, since now the Makefile does them.
nipkow
parents:
972
diff
changeset
|
12 |
proof_timing := true; |
1351 | 13 |
time_use "cla.ML"; |
14 |
time_use "meson.ML"; |
|
15 |
time_use "mesontest.ML"; |
|
1719 | 16 |
(** time_use "mesontest2.ML"; ULTRA SLOW **) |
1026
f2dc38ed53ac
ROOT.ML: Removed the "exit 1" calls, since now the Makefile does them.
nipkow
parents:
972
diff
changeset
|
17 |
time_use_thy "String"; |
1174 | 18 |
time_use_thy "BT"; |
19 |
time_use_thy "Perm"; |
|
1639
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
1621
diff
changeset
|
20 |
time_use_thy "Comb"; |
1026
f2dc38ed53ac
ROOT.ML: Removed the "exit 1" calls, since now the Makefile does them.
nipkow
parents:
972
diff
changeset
|
21 |
time_use_thy "InSort"; |
f2dc38ed53ac
ROOT.ML: Removed the "exit 1" calls, since now the Makefile does them.
nipkow
parents:
972
diff
changeset
|
22 |
time_use_thy "Qsort"; |
f2dc38ed53ac
ROOT.ML: Removed the "exit 1" calls, since now the Makefile does them.
nipkow
parents:
972
diff
changeset
|
23 |
time_use_thy "LexProd"; |
f2dc38ed53ac
ROOT.ML: Removed the "exit 1" calls, since now the Makefile does them.
nipkow
parents:
972
diff
changeset
|
24 |
time_use_thy "Puzzle"; |
1621 | 25 |
time_use_thy "Mutil"; |
1799 | 26 |
time_use_thy "Primes"; |
1026
f2dc38ed53ac
ROOT.ML: Removed the "exit 1" calls, since now the Makefile does them.
nipkow
parents:
972
diff
changeset
|
27 |
time_use_thy "NatSum"; |
1351 | 28 |
time_use "set.ML"; |
1026
f2dc38ed53ac
ROOT.ML: Removed the "exit 1" calls, since now the Makefile does them.
nipkow
parents:
972
diff
changeset
|
29 |
time_use_thy "SList"; |
f2dc38ed53ac
ROOT.ML: Removed the "exit 1" calls, since now the Makefile does them.
nipkow
parents:
972
diff
changeset
|
30 |
time_use_thy "LList"; |
f2dc38ed53ac
ROOT.ML: Removed the "exit 1" calls, since now the Makefile does them.
nipkow
parents:
972
diff
changeset
|
31 |
time_use_thy "Acc"; |
f2dc38ed53ac
ROOT.ML: Removed the "exit 1" calls, since now the Makefile does them.
nipkow
parents:
972
diff
changeset
|
32 |
time_use_thy "PropLog"; |
f2dc38ed53ac
ROOT.ML: Removed the "exit 1" calls, since now the Makefile does them.
nipkow
parents:
972
diff
changeset
|
33 |
time_use_thy "Term"; |
f2dc38ed53ac
ROOT.ML: Removed the "exit 1" calls, since now the Makefile does them.
nipkow
parents:
972
diff
changeset
|
34 |
time_use_thy "Simult"; |
f2dc38ed53ac
ROOT.ML: Removed the "exit 1" calls, since now the Makefile does them.
nipkow
parents:
972
diff
changeset
|
35 |
time_use_thy "MT"; |
1296 | 36 |
|
1165 | 37 |
writeln "END: Root file for HOL examples"; |