author | berghofe |
Tue, 25 Mar 2003 09:50:53 +0100 | |
changeset 13880 | 4f7f30f68926 |
parent 13200 | 7618f289c9c1 |
child 14220 | 4dc132902672 |
permissions | -rw-r--r-- |
12115 | 1 |
(* Title: HOL/ex/ROOT.ML |
2 |
ID: $Id$ |
|
11586 | 3 |
|
12115 | 4 |
Miscellaneous examples for Higher-Order Logic. |
5 |
*) |
|
6 |
||
12360 | 7 |
time_use_thy "Higher_Order_Logic"; |
8 |
||
12115 | 9 |
time_use_thy "Recdefs"; |
10 |
time_use_thy "Primrec"; |
|
12276 | 11 |
time_use_thy "Locales"; |
12115 | 12 |
time_use_thy "Records"; |
13 |
time_use_thy "MonoidGroup"; |
|
14 |
time_use_thy "StringEx"; |
|
15 |
time_use_thy "BinEx"; |
|
16 |
setmp proofs 2 time_use_thy "Hilbert_Classical"; |
|
17 |
time_use_thy "Antiquote"; |
|
18 |
time_use_thy "Multiquote"; |
|
19 |
time_use_thy "Tuple"; |
|
20 |
||
21 |
time_use_thy "NatSum"; |
|
12450
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
12360
diff
changeset
|
22 |
time_use_thy "Intuitionistic"; |
12115 | 23 |
time_use "cla.ML"; |
24 |
time_use "mesontest.ML"; |
|
25 |
time_use_thy "mesontest2"; |
|
13880 | 26 |
time_use_thy "PresburgerEx"; |
12115 | 27 |
time_use_thy "BT"; |
28 |
time_use_thy "AVL"; |
|
29 |
time_use_thy "InSort"; |
|
30 |
time_use_thy "Qsort"; |
|
13200 | 31 |
time_use_thy "MergeSort"; |
12115 | 32 |
time_use_thy "Puzzle"; |
33 |
||
34 |
time_use_thy "IntRing"; |
|
35 |
||
36 |
time_use_thy "set"; |
|
37 |
time_use_thy "MT"; |
|
38 |
time_use_thy "Tarski"; |
|
39 |
||
12869 | 40 |
time_use_thy "SVC_Oracle"; |
12115 | 41 |
if_svc_enabled time_use_thy "svc_test"; |