equal
deleted
inserted
replaced
25 use_thy "Inductive/Mutual"; |
25 use_thy "Inductive/Mutual"; |
26 use_thy "Inductive/Star"; |
26 use_thy "Inductive/Star"; |
27 use_thy "Inductive/AB"; |
27 use_thy "Inductive/AB"; |
28 use_thy "Inductive/Advanced"; |
28 use_thy "Inductive/Advanced"; |
29 |
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"; |
30 use_thy "Misc/Tree"; |
39 use_thy "Misc/Tree2"; |
31 use_thy "Misc/Tree2"; |
40 use_thy "Misc/Plus"; |
32 use_thy "Misc/Plus"; |
41 use_thy "Misc/case_exprs"; |
33 use_thy "Misc/case_exprs"; |
42 use_thy "Misc/fakenat"; |
34 use_thy "Misc/fakenat"; |
51 use_thy "Misc/appendix"; |
43 use_thy "Misc/appendix"; |
52 |
44 |
53 |
45 |
54 Thy_Output.indent_default := 0; |
46 Thy_Output.indent_default := 0; |
55 |
47 |
|
48 use_thy "Protocol/NS_Public"; |
|
49 |
|
50 use_thy "Documents/Documents"; |
|
51 |
|
52 no_document use_thy "Types/Setup"; |
|
53 use_thy "Types/Numbers"; |
|
54 use_thy "Types/Pairs"; |
|
55 use_thy "Types/Records"; |
|
56 use_thy "Types/Typedefs"; |
|
57 use_thy "Types/Overloading"; |
|
58 use_thy "Types/Axioms"; |
|
59 |
56 use_thy "Rules/Basic"; |
60 use_thy "Rules/Basic"; |
57 use_thy "Rules/Blast"; |
61 use_thy "Rules/Blast"; |
58 use_thy "Rules/Force"; |
62 use_thy "Rules/Force"; |
59 use_thy "Rules/Forward"; |
63 use_thy "Rules/Forward"; |
60 use_thy "Rules/Tacticals"; |
64 use_thy "Rules/Tacticals"; |
63 use_thy "Sets/Examples"; |
67 use_thy "Sets/Examples"; |
64 use_thy "Sets/Functions"; |
68 use_thy "Sets/Functions"; |
65 use_thy "Sets/Relations"; |
69 use_thy "Sets/Relations"; |
66 use_thy "Sets/Recur"; |
70 use_thy "Sets/Recur"; |
67 |
71 |
68 use_thy "Protocol/NS_Public"; |
|
69 |
|
70 use_thy "Documents/Documents"; |
|