|
1 Thy_Output.indent_default := 5; |
|
2 |
|
3 use_thy "ToyList/ToyList"; |
|
4 |
|
5 use_thy "Ifexpr/Ifexpr"; |
|
6 |
|
7 use_thy "CodeGen/CodeGen"; |
|
8 |
|
9 use_thy "Trie/Trie"; |
|
10 |
|
11 use_thy "Datatype/ABexpr"; |
|
12 use_thy "Datatype/unfoldnested"; |
|
13 use_thy "Datatype/Nested"; |
|
14 use_thy "Datatype/Fundata"; |
|
15 |
|
16 use_thy "Fun/fun0"; |
|
17 |
|
18 use_thy "Advanced/simp2"; |
|
19 |
|
20 use_thy "CTL/PDL"; |
|
21 use_thy "CTL/CTL"; |
|
22 use_thy "CTL/CTLind"; |
|
23 |
|
24 use_thy "Inductive/Even"; |
|
25 use_thy "Inductive/Mutual"; |
|
26 use_thy "Inductive/Star"; |
|
27 use_thy "Inductive/AB"; |
|
28 use_thy "Inductive/Advanced"; |
|
29 |
|
30 no_document use_thy "Types/Setup"; |
|
31 use_thy "Types/Numbers"; |
|
32 use_thy "Types/Pairs"; |
|
33 use_thy "Types/Records"; |
|
34 use_thy "Types/Typedefs"; |
|
35 use_thy "Types/Overloading"; |
|
36 use_thy "Types/Axioms"; |
|
37 |
|
38 use_thy "Misc/Tree"; |
|
39 use_thy "Misc/Tree2"; |
|
40 use_thy "Misc/Plus"; |
|
41 use_thy "Misc/case_exprs"; |
|
42 use_thy "Misc/fakenat"; |
|
43 use_thy "Misc/natsum"; |
|
44 use_thy "Misc/pairs"; |
|
45 use_thy "Misc/Option2"; |
|
46 use_thy "Misc/types"; |
|
47 use_thy "Misc/prime_def"; |
|
48 use_thy "Misc/simp"; |
|
49 use_thy "Misc/Itrev"; |
|
50 use_thy "Misc/AdvancedInd"; |
|
51 use_thy "Misc/appendix"; |
|
52 |
|
53 |
|
54 Thy_Output.indent_default := 0; |
|
55 |
|
56 use_thy "Rules/Basic"; |
|
57 use_thy "Rules/Blast"; |
|
58 use_thy "Rules/Force"; |
|
59 use_thy "Rules/Forward"; |
|
60 use_thy "Rules/Tacticals"; |
|
61 use_thy "Rules/find2"; |
|
62 |
|
63 use_thy "Sets/Examples"; |
|
64 use_thy "Sets/Functions"; |
|
65 use_thy "Sets/Relations"; |
|
66 use_thy "Sets/Recur"; |
|
67 |
|
68 use_thy "Protocol/NS_Public"; |
|
69 |
|
70 use_thy "Documents/Documents"; |