author | wenzelm |
Fri, 23 Oct 1998 20:28:33 +0200 | |
changeset 5753 | c90b5f7d0c61 |
parent 5368 | 7c8d1c7c876d |
child 5866 | de6a1856c74a |
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"; |
4449 | 12 |
set proof_timing; |
3294 | 13 |
|
5753 | 14 |
(*some examples of recursive function definitions: the TFL package*) |
5124 | 15 |
time_use_thy "Recdefs"; |
4809 | 16 |
time_use_thy "Primes"; |
3294 | 17 |
time_use_thy "Fib"; |
3337 | 18 |
time_use_thy "Primrec"; |
3294 | 19 |
|
20 |
time_use_thy "NatSum"; |
|
1351 | 21 |
time_use "cla.ML"; |
22 |
time_use "meson.ML"; |
|
23 |
time_use "mesontest.ML"; |
|
1719 | 24 |
(** time_use "mesontest2.ML"; ULTRA SLOW **) |
1174 | 25 |
time_use_thy "BT"; |
1026
f2dc38ed53ac
ROOT.ML: Removed the "exit 1" calls, since now the Makefile does them.
nipkow
parents:
972
diff
changeset
|
26 |
time_use_thy "InSort"; |
f2dc38ed53ac
ROOT.ML: Removed the "exit 1" calls, since now the Makefile does them.
nipkow
parents:
972
diff
changeset
|
27 |
time_use_thy "Qsort"; |
f2dc38ed53ac
ROOT.ML: Removed the "exit 1" calls, since now the Makefile does them.
nipkow
parents:
972
diff
changeset
|
28 |
time_use_thy "Puzzle"; |
3294 | 29 |
|
5078 | 30 |
time_use_thy "IntRing"; |
31 |
||
1351 | 32 |
time_use "set.ML"; |
1026
f2dc38ed53ac
ROOT.ML: Removed the "exit 1" calls, since now the Makefile does them.
nipkow
parents:
972
diff
changeset
|
33 |
time_use_thy "MT"; |
1296 | 34 |
|
5199 | 35 |
time_use_thy "StringEx"; |
36 |
time_use_thy "BinEx"; |
|
37 |
||
5753 | 38 |
(*basic use of extensible records*) |
5199 | 39 |
time_use_thy "MonoidGroup"; |
5753 | 40 |
time_use_thy "Points"; |
5199 | 41 |
|
5753 | 42 |
(*groups via locales*) |
5250 | 43 |
time_use_thy "PiSets"; |
44 |
time_use_thy "LocaleGroup"; |
|
45 |
||
5753 | 46 |
(*expressions with quote / antiquote syntax*) |
5368 | 47 |
time_use_thy "Antiquote"; |
48 |
||
5199 | 49 |
|
1165 | 50 |
writeln "END: Root file for HOL examples"; |