12115
|
1 |
(* Title: HOL/ex/ROOT.ML
|
|
2 |
ID: $Id$
|
11586
|
3 |
|
12115
|
4 |
Miscellaneous examples for Higher-Order Logic.
|
|
5 |
*)
|
|
6 |
|
|
7 |
time_use_thy "Recdefs";
|
|
8 |
time_use_thy "Primrec";
|
12276
|
9 |
time_use_thy "Locales";
|
12115
|
10 |
time_use_thy "Records";
|
|
11 |
time_use_thy "MonoidGroup";
|
|
12 |
time_use_thy "StringEx";
|
|
13 |
time_use_thy "BinEx";
|
|
14 |
setmp proofs 2 time_use_thy "Hilbert_Classical";
|
|
15 |
time_use_thy "Antiquote";
|
|
16 |
time_use_thy "Multiquote";
|
|
17 |
time_use_thy "Tuple";
|
|
18 |
|
|
19 |
time_use_thy "NatSum";
|
|
20 |
time_use "cla.ML";
|
|
21 |
time_use "mesontest.ML";
|
|
22 |
time_use_thy "mesontest2";
|
|
23 |
time_use_thy "BT";
|
|
24 |
time_use_thy "AVL";
|
|
25 |
time_use_thy "InSort";
|
|
26 |
time_use_thy "Qsort";
|
|
27 |
time_use_thy "Puzzle";
|
|
28 |
|
|
29 |
time_use_thy "IntRing";
|
|
30 |
|
|
31 |
time_use_thy "set";
|
|
32 |
time_use_thy "MT";
|
|
33 |
time_use_thy "Tarski";
|
|
34 |
|
|
35 |
if_svc_enabled time_use_thy "svc_test";
|