|
1 session Classes! in "Classes/Thy" = HOL + |
|
2 options [browser_info = false, document = false, document_dump = document, document_dump_only] |
|
3 theories [document = false] Setup |
|
4 theories Classes |
|
5 |
|
6 session Codegen! in "Codegen/Thy" = "HOL-Library" + |
|
7 options [browser_info = false, document = false, document_dump = document, document_dump_only, |
|
8 print_mode = "no_brackets,iff"] |
|
9 theories [document = false] Setup |
|
10 theories |
|
11 Introduction |
|
12 Foundations |
|
13 Refinement |
|
14 Inductive_Predicate |
|
15 Evaluation |
|
16 Adaptation |
|
17 Further |
|
18 |
|
19 session Functions! in "Functions/Thy" = HOL + |
|
20 options [browser_info = false, document = false, document_dump = document, document_dump_only] |
|
21 theories Functions |
|
22 |
|
23 session IsarImplementation! in "IsarImplementation/Thy" = HOL + |
|
24 options [browser_info = false, document = false, document_dump = document, document_dump_only] |
|
25 theories |
|
26 Eq |
|
27 Integration |
|
28 Isar |
|
29 Local_Theory |
|
30 Logic |
|
31 ML |
|
32 Prelim |
|
33 Proof |
|
34 Syntax |
|
35 Tactic |
|
36 |
|
37 session IsarRef in "IsarRef/Thy" = HOL + |
|
38 options [browser_info = false, document = false, document_dump = document, document_dump_only, |
|
39 quick_and_dirty] |
|
40 theories |
|
41 Preface |
|
42 Synopsis |
|
43 Framework |
|
44 First_Order_Logic |
|
45 Outer_Syntax |
|
46 Document_Preparation |
|
47 Spec |
|
48 Proof |
|
49 Inner_Syntax |
|
50 Misc |
|
51 Generic |
|
52 HOL_Specific |
|
53 Quick_Reference |
|
54 Symbols |
|
55 ML_Tactic |
|
56 |
|
57 session IsarRef in "IsarRef/Thy" = HOLCF + |
|
58 options [browser_info = false, document = false, document_dump = document, document_dump_only, |
|
59 quick_and_dirty] |
|
60 theories HOLCF_Specific |
|
61 |
|
62 session IsarRef in "IsarRef/Thy" = ZF + |
|
63 options [browser_info = false, document = false, document_dump = document, document_dump_only, |
|
64 quick_and_dirty] |
|
65 theories ZF_Specific |
|
66 |
|
67 session LaTeXsugar! in "LaTeXsugar/Sugar" = HOL + |
|
68 options [browser_info = false, document = false, document_dump = document, document_dump_only, |
|
69 threads = 1] (* FIXME *) |
|
70 theories [document_dump = ""] |
|
71 "~~/src/HOL/Library/LaTeXsugar" |
|
72 "~~/src/HOL/Library/OptionalSugar" |
|
73 theories Sugar |
|
74 |
|
75 session Locales! in "Locales/Locales" = HOL + |
|
76 options [browser_info = false, document = false, document_dump = document, document_dump_only] |
|
77 theories |
|
78 Examples1 |
|
79 Examples2 |
|
80 Examples3 |
|
81 |
|
82 session Main! in "Main/Docs" = HOL + |
|
83 options [browser_info = false, document = false, document_dump = document, document_dump_only] |
|
84 theories Main_Doc |
|
85 |
|
86 session ProgProve! in "ProgProve/Thys" = HOL + |
|
87 options [browser_info = false, document = false, document_dump = document, document_dump_only, |
|
88 show_question_marks = false] |
|
89 theories |
|
90 Basics |
|
91 Bool_nat_list |
|
92 MyList |
|
93 Types_and_funs |
|
94 Logic |
|
95 Isar |
|
96 |
|
97 session System! in "System/Thy" = Pure + |
|
98 options [browser_info = false, document = false, document_dump = document, document_dump_only] |
|
99 theories |
|
100 Basics |
|
101 Interfaces |
|
102 Scala |
|
103 Presentation |
|
104 Misc |
|
105 |
|
106 (* session Tutorial in "Tutorial" = HOL + FIXME *) |
|
107 |
|
108 session examples in "ZF" = ZF + |
|
109 options [browser_info = false, document = false, document_dump = document, document_dump_only, |
|
110 print_mode = "brackets"] |
|
111 theories |
|
112 IFOL_examples |
|
113 FOL_examples |
|
114 ZF_examples |
|
115 If |
|
116 |