equal
deleted
inserted
replaced
5 *) |
5 *) |
6 |
6 |
7 (*some examples of recursive function definitions: the TFL package*) |
7 (*some examples of recursive function definitions: the TFL package*) |
8 time_use_thy "Recdefs"; |
8 time_use_thy "Recdefs"; |
9 time_use_thy "Primrec"; |
9 time_use_thy "Primrec"; |
|
10 |
|
11 setmp proofs 2 time_use_thy "Hilbert_Classical"; |
|
12 |
|
13 (*advanced concrete syntax*) |
|
14 time_use_thy "Tuple"; |
|
15 time_use_thy "Antiquote"; |
|
16 time_use_thy "Multiquote"; |
|
17 |
|
18 (*basic use of extensible records*) |
|
19 time_use_thy "MonoidGroup"; |
|
20 time_use_thy "Records"; |
|
21 |
|
22 time_use_thy "StringEx"; |
|
23 time_use_thy "BinEx"; |
10 |
24 |
11 time_use_thy "NatSum"; |
25 time_use_thy "NatSum"; |
12 time_use "cla.ML"; |
26 time_use "cla.ML"; |
13 time_use "mesontest.ML"; |
27 time_use "mesontest.ML"; |
14 time_use_thy "mesontest2"; |
28 time_use_thy "mesontest2"; |
22 |
36 |
23 time_use_thy "set"; |
37 time_use_thy "set"; |
24 time_use_thy "MT"; |
38 time_use_thy "MT"; |
25 time_use_thy "Tarski"; |
39 time_use_thy "Tarski"; |
26 |
40 |
27 time_use_thy "StringEx"; |
|
28 time_use_thy "BinEx"; |
|
29 |
|
30 if_svc_enabled time_use_thy "svc_test"; |
41 if_svc_enabled time_use_thy "svc_test"; |
31 |
|
32 (*basic use of extensible records*) |
|
33 time_use_thy "MonoidGroup"; |
|
34 time_use_thy "Records"; |
|
35 |
|
36 (*advanced concrete syntax*) |
|
37 time_use_thy "Tuple"; |
|
38 time_use_thy "Antiquote"; |
|
39 time_use_thy "Multiquote"; |
|