author | wenzelm |
Thu, 13 Jul 2000 11:41:40 +0200 | |
changeset 9297 | bafe45732b10 |
parent 9100 | 9e081c812338 |
child 9354 | 4e7e0eb01a6c |
permissions | -rw-r--r-- |
9000 | 1 |
(* Title: HOL/ex/ROOT.ML |
969 | 2 |
ID: $Id$ |
3 |
||
9297 | 4 |
Miscellaneous examples for Higher-Order Logic. |
969 | 5 |
*) |
6 |
||
5753 | 7 |
(*some examples of recursive function definitions: the TFL package*) |
5124 | 8 |
time_use_thy "Recdefs"; |
4809 | 9 |
time_use_thy "Primes"; |
3294 | 10 |
time_use_thy "Fib"; |
9000 | 11 |
with_path "../Induct" time_use_thy "Factorization"; |
3337 | 12 |
time_use_thy "Primrec"; |
3294 | 13 |
|
8944 | 14 |
time_use_thy "NatSum"; |
1351 | 15 |
time_use "cla.ML"; |
16 |
time_use "meson.ML"; |
|
17 |
time_use "mesontest.ML"; |
|
8557
fe75fe482566
restored the MESON examples file HOL/ex/mesontest2.ML
paulson
parents:
8353
diff
changeset
|
18 |
time_use "mesontest2.ML"; |
1174 | 19 |
time_use_thy "BT"; |
8797 | 20 |
time_use_thy "AVL"; |
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 "Puzzle"; |
3294 | 24 |
|
5078 | 25 |
time_use_thy "IntRing"; |
26 |
||
9100 | 27 |
time_use_thy "set"; |
1026
f2dc38ed53ac
ROOT.ML: Removed the "exit 1" calls, since now the Makefile does them.
nipkow
parents:
972
diff
changeset
|
28 |
time_use_thy "MT"; |
7085 | 29 |
time_use_thy "Tarski"; |
1296 | 30 |
|
5199 | 31 |
time_use_thy "StringEx"; |
32 |
time_use_thy "BinEx"; |
|
7187 | 33 |
|
7304 | 34 |
if_svc_enabled time_use_thy "svc_test"; |
5199 | 35 |
|
5753 | 36 |
(*basic use of extensible records*) |
5199 | 37 |
time_use_thy "MonoidGroup"; |
5753 | 38 |
time_use_thy "Points"; |
5199 | 39 |
|
5753 | 40 |
(*groups via locales*) |
5250 | 41 |
time_use_thy "PiSets"; |
42 |
time_use_thy "LocaleGroup"; |
|
43 |
||
5753 | 44 |
(*expressions with quote / antiquote syntax*) |
5368 | 45 |
time_use_thy "Antiquote"; |
8569 | 46 |
time_use_thy "Multiquote"; |